Metamath Proof Explorer

Theorem ordunisuc

Description: An ordinal class is equal to the union of its successor. (Contributed by NM, 10-Dec-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion ordunisuc 
|- ( Ord A -> U. suc A = A )

Proof

Step Hyp Ref Expression
1 ordeleqon 
 |-  ( Ord A <-> ( A e. On \/ A = On ) )
2 suceq 
 |-  ( x = A -> suc x = suc A )
3 2 unieqd 
 |-  ( x = A -> U. suc x = U. suc A )
4 id 
 |-  ( x = A -> x = A )
5 3 4 eqeq12d 
 |-  ( x = A -> ( U. suc x = x <-> U. suc A = A ) )
6 eloni 
 |-  ( x e. On -> Ord x )
7 ordtr 
 |-  ( Ord x -> Tr x )
8 6 7 syl 
 |-  ( x e. On -> Tr x )
9 vex 
 |-  x e. _V
10 9 unisuc 
 |-  ( Tr x <-> U. suc x = x )
11 8 10 sylib 
 |-  ( x e. On -> U. suc x = x )
12 5 11 vtoclga 
 |-  ( A e. On -> U. suc A = A )
13 sucon 
 |-  suc On = On
14 13 unieqi 
 |-  U. suc On = U. On
15 unon 
 |-  U. On = On
16 14 15 eqtri 
 |-  U. suc On = On
17 suceq 
 |-  ( A = On -> suc A = suc On )
18 17 unieqd 
 |-  ( A = On -> U. suc A = U. suc On )
19 id 
 |-  ( A = On -> A = On )
20 16 18 19 3eqtr4a 
 |-  ( A = On -> U. suc A = A )
21 12 20 jaoi 
 |-  ( ( A e. On \/ A = On ) -> U. suc A = A )
22 1 21 sylbi 
 |-  ( Ord A -> U. suc A = A )