Intuitionize soss in iset.mm
Intuitionize soss in iset.mm

Pretty much the same proof works with the obvious changes from
df-so to df-iso (three variables instead of two, mainly).

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