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