Metamath Proof Explorer

Theorem onsucunipr

Description: The successor to the union of any pair of ordinals is the union of the successors of the elements. (Contributed by RP, 12-Feb-2025)

Ref Expression
Assertion onsucunipr ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → suc ∪ { 𝐴 , 𝐵 } = ∪ { suc 𝐴 , suc 𝐵 } )

Proof

Step Hyp Ref Expression
1 ssequn1 ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∪ 𝐵 ) = 𝐵 )
2 suceq ⊢ ( ( 𝐴 ∪ 𝐵 ) = 𝐵 → suc ( 𝐴 ∪ 𝐵 ) = suc 𝐵 )
3 1 2 sylbi ⊢ ( 𝐴 ⊆ 𝐵 → suc ( 𝐴 ∪ 𝐵 ) = suc 𝐵 )
4 3 adantl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → suc ( 𝐴 ∪ 𝐵 ) = suc 𝐵 )
5 onsucwordi ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 → suc 𝐴 ⊆ suc 𝐵 ) )
6 5 imp ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → suc 𝐴 ⊆ suc 𝐵 )
7 ssequn1 ⊢ ( suc 𝐴 ⊆ suc 𝐵 ↔ ( suc 𝐴 ∪ suc 𝐵 ) = suc 𝐵 )
8 6 7 sylib ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( suc 𝐴 ∪ suc 𝐵 ) = suc 𝐵 )
9 4 8 eqtr4d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → suc ( 𝐴 ∪ 𝐵 ) = ( suc 𝐴 ∪ suc 𝐵 ) )
10 ssequn2 ⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐴 ∪ 𝐵 ) = 𝐴 )
11 suceq ⊢ ( ( 𝐴 ∪ 𝐵 ) = 𝐴 → suc ( 𝐴 ∪ 𝐵 ) = suc 𝐴 )
12 10 11 sylbi ⊢ ( 𝐵 ⊆ 𝐴 → suc ( 𝐴 ∪ 𝐵 ) = suc 𝐴 )
13 12 adantl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐵 ⊆ 𝐴 ) → suc ( 𝐴 ∪ 𝐵 ) = suc 𝐴 )
14 onsucwordi ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐵 ⊆ 𝐴 → suc 𝐵 ⊆ suc 𝐴 ) )
15 14 ancoms ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 ⊆ 𝐴 → suc 𝐵 ⊆ suc 𝐴 ) )
16 15 imp ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐵 ⊆ 𝐴 ) → suc 𝐵 ⊆ suc 𝐴 )
17 ssequn2 ⊢ ( suc 𝐵 ⊆ suc 𝐴 ↔ ( suc 𝐴 ∪ suc 𝐵 ) = suc 𝐴 )
18 16 17 sylib ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐵 ⊆ 𝐴 ) → ( suc 𝐴 ∪ suc 𝐵 ) = suc 𝐴 )
19 13 18 eqtr4d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐵 ⊆ 𝐴 ) → suc ( 𝐴 ∪ 𝐵 ) = ( suc 𝐴 ∪ suc 𝐵 ) )
20 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
21 eloni ⊢ ( 𝐵 ∈ On → Ord 𝐵 )
22 ordtri2or2 ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )
23 20 21 22 syl2an ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )
24 9 19 23 mpjaodan ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → suc ( 𝐴 ∪ 𝐵 ) = ( suc 𝐴 ∪ suc 𝐵 ) )
25 uniprg ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
26 suceq ⊢ ( ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) → suc ∪ { 𝐴 , 𝐵 } = suc ( 𝐴 ∪ 𝐵 ) )
27 25 26 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → suc ∪ { 𝐴 , 𝐵 } = suc ( 𝐴 ∪ 𝐵 ) )
28 onsuc ⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ On )
29 onsuc ⊢ ( 𝐵 ∈ On → suc 𝐵 ∈ On )
30 uniprg ⊢ ( ( suc 𝐴 ∈ On ∧ suc 𝐵 ∈ On ) → ∪ { suc 𝐴 , suc 𝐵 } = ( suc 𝐴 ∪ suc 𝐵 ) )
31 28 29 30 syl2an ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ∪ { suc 𝐴 , suc 𝐵 } = ( suc 𝐴 ∪ suc 𝐵 ) )
32 24 27 31 3eqtr4d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → suc ∪ { 𝐴 , 𝐵 } = ∪ { suc 𝐴 , suc 𝐵 } )