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