Add nfrimi to iset.mm.
Add nfrimi to iset.mm.

Not a perfect analogue to alrimi, but nfrimi seemed like a pretty
good name.

This came up because I wanted it as a lemma for another proof, but
it seems like it could well be generaly useful.

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