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 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → suc ⁡ ⋃ A B C = ⋃ suc ⁡ A suc ⁡ B suc ⁡ C

Proof

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