Metamath Proof Explorer


Theorem dfon4

Description: Another quantifier-free definition of On . (Contributed by Scott Fenton, 4-May-2014)

Ref Expression
Assertion dfon4 On = V 𝖲𝖲𝖾𝗍 I E 𝖳𝗋𝖺𝗇𝗌

Proof

Step Hyp Ref Expression
1 dfon3 On = V ran 𝖲𝖲𝖾𝗍 𝖳𝗋𝖺𝗇𝗌 × V I E
2 df-ima 𝖲𝖲𝖾𝗍 I E 𝖳𝗋𝖺𝗇𝗌 = ran 𝖲𝖲𝖾𝗍 I E 𝖳𝗋𝖺𝗇𝗌
3 df-res 𝖲𝖲𝖾𝗍 I E 𝖳𝗋𝖺𝗇𝗌 = 𝖲𝖲𝖾𝗍 I E 𝖳𝗋𝖺𝗇𝗌 × V
4 indif1 𝖲𝖲𝖾𝗍 I E 𝖳𝗋𝖺𝗇𝗌 × V = 𝖲𝖲𝖾𝗍 𝖳𝗋𝖺𝗇𝗌 × V I E
5 3 4 eqtri 𝖲𝖲𝖾𝗍 I E 𝖳𝗋𝖺𝗇𝗌 = 𝖲𝖲𝖾𝗍 𝖳𝗋𝖺𝗇𝗌 × V I E
6 5 rneqi ran 𝖲𝖲𝖾𝗍 I E 𝖳𝗋𝖺𝗇𝗌 = ran 𝖲𝖲𝖾𝗍 𝖳𝗋𝖺𝗇𝗌 × V I E
7 2 6 eqtri 𝖲𝖲𝖾𝗍 I E 𝖳𝗋𝖺𝗇𝗌 = ran 𝖲𝖲𝖾𝗍 𝖳𝗋𝖺𝗇𝗌 × V I E
8 7 difeq2i V 𝖲𝖲𝖾𝗍 I E 𝖳𝗋𝖺𝗇𝗌 = V ran 𝖲𝖲𝖾𝗍 𝖳𝗋𝖺𝗇𝗌 × V I E
9 1 8 eqtr4i On = V 𝖲𝖲𝖾𝗍 I E 𝖳𝗋𝖺𝗇𝗌