Metamath Proof Explorer

Theorem onsucunitp

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

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

Proof

Step Hyp Ref Expression
1 onun2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∪ 𝐵 ) ∈ On )
2 onsucunipr ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ∈ On ∧ 𝐶 ∈ On ) → suc ∪ { ( 𝐴 ∪ 𝐵 ) , 𝐶 } = ∪ { suc ( 𝐴 ∪ 𝐵 ) , suc 𝐶 } )
3 1 2 sylan ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → suc ∪ { ( 𝐴 ∪ 𝐵 ) , 𝐶 } = ∪ { suc ( 𝐴 ∪ 𝐵 ) , suc 𝐶 } )
4 uniprg ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
5 4 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
6 unisng ⊢ ( 𝐶 ∈ On → ∪ { 𝐶 } = 𝐶 )
7 6 adantl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ∪ { 𝐶 } = 𝐶 )
8 5 7 uneq12d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ( ∪ { 𝐴 , 𝐵 } ∪ ∪ { 𝐶 } ) = ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )
9 df-tp ⊢ { 𝐴 , 𝐵 , 𝐶 } = ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
10 9 unieqi ⊢ ∪ { 𝐴 , 𝐵 , 𝐶 } = ∪ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } )
11 uniun ⊢ ∪ ( { 𝐴 , 𝐵 } ∪ { 𝐶 } ) = ( ∪ { 𝐴 , 𝐵 } ∪ ∪ { 𝐶 } )
12 10 11 eqtri ⊢ ∪ { 𝐴 , 𝐵 , 𝐶 } = ( ∪ { 𝐴 , 𝐵 } ∪ ∪ { 𝐶 } )
13 12 a1i ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ∪ { 𝐴 , 𝐵 , 𝐶 } = ( ∪ { 𝐴 , 𝐵 } ∪ ∪ { 𝐶 } ) )
14 uniprg ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ∈ On ∧ 𝐶 ∈ On ) → ∪ { ( 𝐴 ∪ 𝐵 ) , 𝐶 } = ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )
15 1 14 sylan ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ∪ { ( 𝐴 ∪ 𝐵 ) , 𝐶 } = ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )
16 8 13 15 3eqtr4d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ∪ { 𝐴 , 𝐵 , 𝐶 } = ∪ { ( 𝐴 ∪ 𝐵 ) , 𝐶 } )
17 suceq ⊢ ( ∪ { 𝐴 , 𝐵 , 𝐶 } = ∪ { ( 𝐴 ∪ 𝐵 ) , 𝐶 } → suc ∪ { 𝐴 , 𝐵 , 𝐶 } = suc ∪ { ( 𝐴 ∪ 𝐵 ) , 𝐶 } )
18 16 17 syl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → suc ∪ { 𝐴 , 𝐵 , 𝐶 } = suc ∪ { ( 𝐴 ∪ 𝐵 ) , 𝐶 } )
19 df-tp ⊢ { suc 𝐴 , suc 𝐵 , suc 𝐶 } = ( { suc 𝐴 , suc 𝐵 } ∪ { suc 𝐶 } )
20 19 unieqi ⊢ ∪ { suc 𝐴 , suc 𝐵 , suc 𝐶 } = ∪ ( { suc 𝐴 , suc 𝐵 } ∪ { suc 𝐶 } )
21 uniun ⊢ ∪ ( { suc 𝐴 , suc 𝐵 } ∪ { suc 𝐶 } ) = ( ∪ { suc 𝐴 , suc 𝐵 } ∪ ∪ { suc 𝐶 } )
22 20 21 eqtri ⊢ ∪ { suc 𝐴 , suc 𝐵 , suc 𝐶 } = ( ∪ { suc 𝐴 , suc 𝐵 } ∪ ∪ { suc 𝐶 } )
23 onsuc ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ On → suc ( 𝐴 ∪ 𝐵 ) ∈ On )
24 1 23 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → suc ( 𝐴 ∪ 𝐵 ) ∈ On )
25 onsuc ⊢ ( 𝐶 ∈ On → suc 𝐶 ∈ On )
26 uniprg ⊢ ( ( suc ( 𝐴 ∪ 𝐵 ) ∈ On ∧ suc 𝐶 ∈ On ) → ∪ { suc ( 𝐴 ∪ 𝐵 ) , suc 𝐶 } = ( suc ( 𝐴 ∪ 𝐵 ) ∪ suc 𝐶 ) )
27 24 25 26 syl2an ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ∪ { suc ( 𝐴 ∪ 𝐵 ) , suc 𝐶 } = ( suc ( 𝐴 ∪ 𝐵 ) ∪ suc 𝐶 ) )
28 suceq ⊢ ( ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) → suc ∪ { 𝐴 , 𝐵 } = suc ( 𝐴 ∪ 𝐵 ) )
29 4 28 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → suc ∪ { 𝐴 , 𝐵 } = suc ( 𝐴 ∪ 𝐵 ) )
30 onsucunipr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → suc ∪ { 𝐴 , 𝐵 } = ∪ { suc 𝐴 , suc 𝐵 } )
31 29 30 eqtr3d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → suc ( 𝐴 ∪ 𝐵 ) = ∪ { suc 𝐴 , suc 𝐵 } )
32 31 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → suc ( 𝐴 ∪ 𝐵 ) = ∪ { suc 𝐴 , suc 𝐵 } )
33 unisng ⊢ ( suc 𝐶 ∈ On → ∪ { suc 𝐶 } = suc 𝐶 )
34 25 33 syl ⊢ ( 𝐶 ∈ On → ∪ { suc 𝐶 } = suc 𝐶 )
35 34 eqcomd ⊢ ( 𝐶 ∈ On → suc 𝐶 = ∪ { suc 𝐶 } )
36 35 adantl ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → suc 𝐶 = ∪ { suc 𝐶 } )
37 32 36 uneq12d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ( suc ( 𝐴 ∪ 𝐵 ) ∪ suc 𝐶 ) = ( ∪ { suc 𝐴 , suc 𝐵 } ∪ ∪ { suc 𝐶 } ) )
38 27 37 eqtrd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ∪ { suc ( 𝐴 ∪ 𝐵 ) , suc 𝐶 } = ( ∪ { suc 𝐴 , suc 𝐵 } ∪ ∪ { suc 𝐶 } ) )
39 22 38 eqtr4id ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ∪ { suc 𝐴 , suc 𝐵 , suc 𝐶 } = ∪ { suc ( 𝐴 ∪ 𝐵 ) , suc 𝐶 } )
40 3 18 39 3eqtr4d ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → suc ∪ { 𝐴 , 𝐵 , 𝐶 } = ∪ { suc 𝐴 , suc 𝐵 , suc 𝐶 } )
41 40 3impa ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → suc ∪ { 𝐴 , 𝐵 , 𝐶 } = ∪ { suc 𝐴 , suc 𝐵 , suc 𝐶 } )