Add phibnd to iset.mm
Add phibnd to iset.mm

phibnd is stated as in set.mm. The proof is similar to the set.mm one
but is changed in various places to show that sets are finite and the
like.

Add lemma phibndlem which is stated as in set.mm and whose proof is basically
the set.mm one but with some rearrangement to use mpjaodan rather than
ord .

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