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