Add onprc to iset.mm
Add onprc to iset.mm

The proof from set.mm works as-is (although in our case it uses
the Axiom of Set Induction and will as long as ordirr does, so
revies the comment accordingly).

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