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 suceloni
 |-  ( 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