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 
|- U. On = On

Proof

Step Hyp Ref Expression
1 eluni2 
 |-  ( x e. U. On <-> E. y e. On x e. y )
2 onelon 
 |-  ( ( y e. On /\ x e. y ) -> x e. On )
3 2 rexlimiva 
 |-  ( E. y e. On x e. y -> x e. On )
4 1 3 sylbi 
 |-  ( x e. U. On -> x e. On )
5 vex 
 |-  x e. _V
6 5 sucid 
 |-  x e. suc x
7 onsuc 
 |-  ( x e. On -> suc x e. On )
8 elunii 
 |-  ( ( x e. suc x /\ suc x e. On ) -> x e. U. On )
9 6 7 8 sylancr 
 |-  ( x e. On -> x e. U. On )
10 4 9 impbii 
 |-  ( x e. U. On <-> x e. On )
11 10 eqriv 
 |-  U. On = On