Add f1dmvrnfibi to iset.mm
Add f1dmvrnfibi to iset.mm

The theorem is stated as in set.mm. The proof in the ran F e. Fin -> F
e. Fin direction is identical to the set.mm proof. The proof in the F e.
Fin -> ran F e. Fin direction needs to be adjusted for the differences
between rnfi (set.mm) and funrnfi (iset.mm) but there is nothing
especially difficult there.

Update the comment with version from AV

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