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 𝐴 ∧ Ord 𝐵 ) → suc ( 𝐴 ∪ 𝐵 ) = ( suc 𝐴 ∪ suc 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ordun ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → Ord ( 𝐴 ∪ 𝐵 ) )
2 ordsuc ⊢ ( Ord ( 𝐴 ∪ 𝐵 ) ↔ Ord suc ( 𝐴 ∪ 𝐵 ) )
3 ordelon ⊢ ( ( Ord suc ( 𝐴 ∪ 𝐵 ) ∧ 𝑥 ∈ suc ( 𝐴 ∪ 𝐵 ) ) → 𝑥 ∈ On )
4 3 ex ⊢ ( Ord suc ( 𝐴 ∪ 𝐵 ) → ( 𝑥 ∈ suc ( 𝐴 ∪ 𝐵 ) → 𝑥 ∈ On ) )
5 2 4 sylbi ⊢ ( Ord ( 𝐴 ∪ 𝐵 ) → ( 𝑥 ∈ suc ( 𝐴 ∪ 𝐵 ) → 𝑥 ∈ On ) )
6 1 5 syl ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑥 ∈ suc ( 𝐴 ∪ 𝐵 ) → 𝑥 ∈ On ) )
7 ordsuc ⊢ ( Ord 𝐴 ↔ Ord suc 𝐴 )
8 ordsuc ⊢ ( Ord 𝐵 ↔ Ord suc 𝐵 )
9 ordun ⊢ ( ( Ord suc 𝐴 ∧ Ord suc 𝐵 ) → Ord ( suc 𝐴 ∪ suc 𝐵 ) )
10 ordelon ⊢ ( ( Ord ( suc 𝐴 ∪ suc 𝐵 ) ∧ 𝑥 ∈ ( suc 𝐴 ∪ suc 𝐵 ) ) → 𝑥 ∈ On )
11 10 ex ⊢ ( Ord ( suc 𝐴 ∪ suc 𝐵 ) → ( 𝑥 ∈ ( suc 𝐴 ∪ suc 𝐵 ) → 𝑥 ∈ On ) )
12 9 11 syl ⊢ ( ( Ord suc 𝐴 ∧ Ord suc 𝐵 ) → ( 𝑥 ∈ ( suc 𝐴 ∪ suc 𝐵 ) → 𝑥 ∈ On ) )
13 7 8 12 syl2anb ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑥 ∈ ( suc 𝐴 ∪ suc 𝐵 ) → 𝑥 ∈ On ) )
14 ordssun ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑥 ⊆ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ⊆ 𝐴 ∨ 𝑥 ⊆ 𝐵 ) ) )
15 14 adantl ⊢ ( ( 𝑥 ∈ On ∧ ( Ord 𝐴 ∧ Ord 𝐵 ) ) → ( 𝑥 ⊆ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ⊆ 𝐴 ∨ 𝑥 ⊆ 𝐵 ) ) )
16 ordsssuc ⊢ ( ( 𝑥 ∈ On ∧ Ord ( 𝐴 ∪ 𝐵 ) ) → ( 𝑥 ⊆ ( 𝐴 ∪ 𝐵 ) ↔ 𝑥 ∈ suc ( 𝐴 ∪ 𝐵 ) ) )
17 1 16 sylan2 ⊢ ( ( 𝑥 ∈ On ∧ ( Ord 𝐴 ∧ Ord 𝐵 ) ) → ( 𝑥 ⊆ ( 𝐴 ∪ 𝐵 ) ↔ 𝑥 ∈ suc ( 𝐴 ∪ 𝐵 ) ) )
18 ordsssuc ⊢ ( ( 𝑥 ∈ On ∧ Ord 𝐴 ) → ( 𝑥 ⊆ 𝐴 ↔ 𝑥 ∈ suc 𝐴 ) )
19 18 adantrr ⊢ ( ( 𝑥 ∈ On ∧ ( Ord 𝐴 ∧ Ord 𝐵 ) ) → ( 𝑥 ⊆ 𝐴 ↔ 𝑥 ∈ suc 𝐴 ) )
20 ordsssuc ⊢ ( ( 𝑥 ∈ On ∧ Ord 𝐵 ) → ( 𝑥 ⊆ 𝐵 ↔ 𝑥 ∈ suc 𝐵 ) )
21 20 adantrl ⊢ ( ( 𝑥 ∈ On ∧ ( Ord 𝐴 ∧ Ord 𝐵 ) ) → ( 𝑥 ⊆ 𝐵 ↔ 𝑥 ∈ suc 𝐵 ) )
22 19 21 orbi12d ⊢ ( ( 𝑥 ∈ On ∧ ( Ord 𝐴 ∧ Ord 𝐵 ) ) → ( ( 𝑥 ⊆ 𝐴 ∨ 𝑥 ⊆ 𝐵 ) ↔ ( 𝑥 ∈ suc 𝐴 ∨ 𝑥 ∈ suc 𝐵 ) ) )
23 15 17 22 3bitr3d ⊢ ( ( 𝑥 ∈ On ∧ ( Ord 𝐴 ∧ Ord 𝐵 ) ) → ( 𝑥 ∈ suc ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ∈ suc 𝐴 ∨ 𝑥 ∈ suc 𝐵 ) ) )
24 elun ⊢ ( 𝑥 ∈ ( suc 𝐴 ∪ suc 𝐵 ) ↔ ( 𝑥 ∈ suc 𝐴 ∨ 𝑥 ∈ suc 𝐵 ) )
25 23 24 bitr4di ⊢ ( ( 𝑥 ∈ On ∧ ( Ord 𝐴 ∧ Ord 𝐵 ) ) → ( 𝑥 ∈ suc ( 𝐴 ∪ 𝐵 ) ↔ 𝑥 ∈ ( suc 𝐴 ∪ suc 𝐵 ) ) )
26 25 expcom ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑥 ∈ On → ( 𝑥 ∈ suc ( 𝐴 ∪ 𝐵 ) ↔ 𝑥 ∈ ( suc 𝐴 ∪ suc 𝐵 ) ) ) )
27 6 13 26 pm5.21ndd ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝑥 ∈ suc ( 𝐴 ∪ 𝐵 ) ↔ 𝑥 ∈ ( suc 𝐴 ∪ suc 𝐵 ) ) )
28 27 eqrdv ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → suc ( 𝐴 ∪ 𝐵 ) = ( suc 𝐴 ∪ suc 𝐵 ) )