Add fnfi to iset.mm
Add fnfi to iset.mm

The theorem is stated as in set.mm. The proof is generally similar to
the set.mm one but tweaked in various spots, especially to change
unfi to unsnfi but also to use findcard2sd and a few other changes here
and there.

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