Add pairs section to iset.mm
Add pairs section to iset.mm

This is the "Unordered and ordered pairs" section, copied
from set.mm

It does include pulling the comma and the typesetting from
elsewhere in set.mm but does not include generally fixing
up the proofs or comments. Follow up changes will address that.

It does include removing ifpr and dfopif.
Since we didn't pick up the deduction theorem section (which would
involve significant work to intuitionize if it is even possible,
and which is not considered to be particularly recommended), we
don't have the things which ifpr and dfopif rely on.

metamath/set.mm,metamath/set.mm,metamath/set.mm