Metamath Proof Explorer


Theorem unon

Description: The class of all ordinal numbers is its own union. Exercise 11 of TakeutiZaring p. 40. (Contributed by NM, 12-Nov-2003)

Ref Expression
Assertion unon On=On

Proof

Step Hyp Ref Expression
1 eluni2 xOnyOnxy
2 onelon yOnxyxOn
3 2 rexlimiva yOnxyxOn
4 1 3 sylbi xOnxOn
5 vex xV
6 5 sucid xsucx
7 suceloni xOnsucxOn
8 elunii xsucxsucxOnxOn
9 6 7 8 sylancr xOnxOn
10 4 9 impbii xOnxOn
11 10 eqriv On=On