Add recexsrlem to iset.mm
Add recexsrlem to iset.mm

The proof in set.mm works with various bits intutionized but the
overall structure of the proof not changed.

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