This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem onsucuni2

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

Ref Expression
Assertion onsucuni2 
|- ( ( A e. On /\ A = suc B ) -> suc U. A = A )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( A = suc B -> ( A e. On <-> suc B e. On ) )
2 1 biimpac 
 |-  ( ( A e. On /\ A = suc B ) -> suc B e. On )
3 eloni 
 |-  ( suc B e. On -> Ord suc B )
4 ordsuc 
 |-  ( Ord B <-> Ord suc B )
5 ordunisuc 
 |-  ( Ord B -> U. suc B = B )
6 4 5 sylbir 
 |-  ( Ord suc B -> U. suc B = B )
7 suceq 
 |-  ( U. suc B = B -> suc U. suc B = suc B )
8 6 7 syl 
 |-  ( Ord suc B -> suc U. suc B = suc B )
9 ordunisuc 
 |-  ( Ord suc B -> U. suc suc B = suc B )
10 8 9 eqtr4d 
 |-  ( Ord suc B -> suc U. suc B = U. suc suc B )
11 2 3 10 3syl 
 |-  ( ( A e. On /\ A = suc B ) -> suc U. suc B = U. suc suc B )
12 unieq 
 |-  ( A = suc B -> U. A = U. suc B )
13 suceq 
 |-  ( U. A = U. suc B -> suc U. A = suc U. suc B )
14 12 13 syl 
 |-  ( A = suc B -> suc U. A = suc U. suc B )
15 suceq 
 |-  ( A = suc B -> suc A = suc suc B )
16 15 unieqd 
 |-  ( A = suc B -> U. suc A = U. suc suc B )
17 14 16 eqeq12d 
 |-  ( A = suc B -> ( suc U. A = U. suc A <-> suc U. suc B = U. suc suc B ) )
18 11 17 imbitrrid 
 |-  ( A = suc B -> ( ( A e. On /\ A = suc B ) -> suc U. A = U. suc A ) )
19 18 anabsi7 
 |-  ( ( A e. On /\ A = suc B ) -> suc U. A = U. suc A )
20 eloni 
 |-  ( A e. On -> Ord A )
21 ordunisuc 
 |-  ( Ord A -> U. suc A = A )
22 20 21 syl 
 |-  ( A e. On -> U. suc A = A )
23 22 adantr 
 |-  ( ( A e. On /\ A = suc B ) -> U. suc A = A )
24 19 23 eqtrd 
 |-  ( ( A e. On /\ A = suc B ) -> suc U. A = A )