Metamath Proof Explorer

Theorem ordsucun

Description: The successor of the maximum (i.e. union) of two ordinals is the maximum of their successors. (Contributed by NM, 28-Nov-2003)

Ref Expression
Assertion ordsucun 
|- ( ( Ord A /\ Ord B ) -> suc ( A u. B ) = ( suc A u. suc B ) )

Proof

Step Hyp Ref Expression
1 ordun 
 |-  ( ( Ord A /\ Ord B ) -> Ord ( A u. B ) )
2 ordsuc 
 |-  ( Ord ( A u. B ) <-> Ord suc ( A u. B ) )
3 ordelon 
 |-  ( ( Ord suc ( A u. B ) /\ x e. suc ( A u. B ) ) -> x e. On )
4 3 ex 
 |-  ( Ord suc ( A u. B ) -> ( x e. suc ( A u. B ) -> x e. On ) )
5 2 4 sylbi 
 |-  ( Ord ( A u. B ) -> ( x e. suc ( A u. B ) -> x e. On ) )
6 1 5 syl 
 |-  ( ( Ord A /\ Ord B ) -> ( x e. suc ( A u. B ) -> x e. On ) )
7 ordsuc 
 |-  ( Ord A <-> Ord suc A )
8 ordsuc 
 |-  ( Ord B <-> Ord suc B )
9 ordun 
 |-  ( ( Ord suc A /\ Ord suc B ) -> Ord ( suc A u. suc B ) )
10 ordelon 
 |-  ( ( Ord ( suc A u. suc B ) /\ x e. ( suc A u. suc B ) ) -> x e. On )
11 10 ex 
 |-  ( Ord ( suc A u. suc B ) -> ( x e. ( suc A u. suc B ) -> x e. On ) )
12 9 11 syl 
 |-  ( ( Ord suc A /\ Ord suc B ) -> ( x e. ( suc A u. suc B ) -> x e. On ) )
13 7 8 12 syl2anb 
 |-  ( ( Ord A /\ Ord B ) -> ( x e. ( suc A u. suc B ) -> x e. On ) )
14 ordssun 
 |-  ( ( Ord A /\ Ord B ) -> ( x C_ ( A u. B ) <-> ( x C_ A \/ x C_ B ) ) )
15 14 adantl 
 |-  ( ( x e. On /\ ( Ord A /\ Ord B ) ) -> ( x C_ ( A u. B ) <-> ( x C_ A \/ x C_ B ) ) )
16 ordsssuc 
 |-  ( ( x e. On /\ Ord ( A u. B ) ) -> ( x C_ ( A u. B ) <-> x e. suc ( A u. B ) ) )
17 1 16 sylan2 
 |-  ( ( x e. On /\ ( Ord A /\ Ord B ) ) -> ( x C_ ( A u. B ) <-> x e. suc ( A u. B ) ) )
18 ordsssuc 
 |-  ( ( x e. On /\ Ord A ) -> ( x C_ A <-> x e. suc A ) )
19 18 adantrr 
 |-  ( ( x e. On /\ ( Ord A /\ Ord B ) ) -> ( x C_ A <-> x e. suc A ) )
20 ordsssuc 
 |-  ( ( x e. On /\ Ord B ) -> ( x C_ B <-> x e. suc B ) )
21 20 adantrl 
 |-  ( ( x e. On /\ ( Ord A /\ Ord B ) ) -> ( x C_ B <-> x e. suc B ) )
22 19 21 orbi12d 
 |-  ( ( x e. On /\ ( Ord A /\ Ord B ) ) -> ( ( x C_ A \/ x C_ B ) <-> ( x e. suc A \/ x e. suc B ) ) )
23 15 17 22 3bitr3d 
 |-  ( ( x e. On /\ ( Ord A /\ Ord B ) ) -> ( x e. suc ( A u. B ) <-> ( x e. suc A \/ x e. suc B ) ) )
24 elun 
 |-  ( x e. ( suc A u. suc B ) <-> ( x e. suc A \/ x e. suc B ) )
25 23 24 bitr4di 
 |-  ( ( x e. On /\ ( Ord A /\ Ord B ) ) -> ( x e. suc ( A u. B ) <-> x e. ( suc A u. suc B ) ) )
26 25 expcom 
 |-  ( ( Ord A /\ Ord B ) -> ( x e. On -> ( x e. suc ( A u. B ) <-> x e. ( suc A u. suc B ) ) ) )
27 6 13 26 pm5.21ndd 
 |-  ( ( Ord A /\ Ord B ) -> ( x e. suc ( A u. B ) <-> x e. ( suc A u. suc B ) ) )
28 27 eqrdv 
 |-  ( ( Ord A /\ Ord B ) -> suc ( A u. B ) = ( suc A u. suc B ) )