Proof of Theorem onsucunitp
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | onun2 6491 | . . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∪ 𝐵) ∈ On) | 
| 2 |  | onsucunipr 43390 | . . . 4
⊢ (((𝐴 ∪ 𝐵) ∈ On ∧ 𝐶 ∈ On) → suc ∪ {(𝐴
∪ 𝐵), 𝐶} = ∪ {suc (𝐴 ∪ 𝐵), suc 𝐶}) | 
| 3 | 1, 2 | sylan 580 | . . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → suc ∪ {(𝐴
∪ 𝐵), 𝐶} = ∪ {suc (𝐴 ∪ 𝐵), suc 𝐶}) | 
| 4 |  | uniprg 4922 | . . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∪ {𝐴,
𝐵} = (𝐴 ∪ 𝐵)) | 
| 5 | 4 | adantr 480 | . . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ∪ {𝐴,
𝐵} = (𝐴 ∪ 𝐵)) | 
| 6 |  | unisng 4924 | . . . . . . 7
⊢ (𝐶 ∈ On → ∪ {𝐶}
= 𝐶) | 
| 7 | 6 | adantl 481 | . . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ∪ {𝐶}
= 𝐶) | 
| 8 | 5, 7 | uneq12d 4168 | . . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (∪ {𝐴,
𝐵} ∪ ∪ {𝐶})
= ((𝐴 ∪ 𝐵) ∪ 𝐶)) | 
| 9 |  | df-tp 4630 | . . . . . . . 8
⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) | 
| 10 | 9 | unieqi 4918 | . . . . . . 7
⊢ ∪ {𝐴,
𝐵, 𝐶} = ∪ ({𝐴, 𝐵} ∪ {𝐶}) | 
| 11 |  | uniun 4929 | . . . . . . 7
⊢ ∪ ({𝐴,
𝐵} ∪ {𝐶}) = (∪ {𝐴, 𝐵} ∪ ∪ {𝐶}) | 
| 12 | 10, 11 | eqtri 2764 | . . . . . 6
⊢ ∪ {𝐴,
𝐵, 𝐶} = (∪ {𝐴, 𝐵} ∪ ∪ {𝐶}) | 
| 13 | 12 | a1i 11 | . . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ∪ {𝐴,
𝐵, 𝐶} = (∪ {𝐴, 𝐵} ∪ ∪ {𝐶})) | 
| 14 |  | uniprg 4922 | . . . . . 6
⊢ (((𝐴 ∪ 𝐵) ∈ On ∧ 𝐶 ∈ On) → ∪ {(𝐴
∪ 𝐵), 𝐶} = ((𝐴 ∪ 𝐵) ∪ 𝐶)) | 
| 15 | 1, 14 | sylan 580 | . . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ∪ {(𝐴
∪ 𝐵), 𝐶} = ((𝐴 ∪ 𝐵) ∪ 𝐶)) | 
| 16 | 8, 13, 15 | 3eqtr4d 2786 | . . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ∪ {𝐴,
𝐵, 𝐶} = ∪ {(𝐴 ∪ 𝐵), 𝐶}) | 
| 17 |  | suceq 6449 | . . . 4
⊢ (∪ {𝐴,
𝐵, 𝐶} = ∪ {(𝐴 ∪ 𝐵), 𝐶} → suc ∪
{𝐴, 𝐵, 𝐶} = suc ∪ {(𝐴 ∪ 𝐵), 𝐶}) | 
| 18 | 16, 17 | syl 17 | . . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → suc ∪ {𝐴,
𝐵, 𝐶} = suc ∪ {(𝐴 ∪ 𝐵), 𝐶}) | 
| 19 |  | df-tp 4630 | . . . . . 6
⊢ {suc
𝐴, suc 𝐵, suc 𝐶} = ({suc 𝐴, suc 𝐵} ∪ {suc 𝐶}) | 
| 20 | 19 | unieqi 4918 | . . . . 5
⊢ ∪ {suc 𝐴, suc 𝐵, suc 𝐶} = ∪ ({suc 𝐴, suc 𝐵} ∪ {suc 𝐶}) | 
| 21 |  | uniun 4929 | . . . . 5
⊢ ∪ ({suc 𝐴, suc 𝐵} ∪ {suc 𝐶}) = (∪ {suc
𝐴, suc 𝐵} ∪ ∪ {suc
𝐶}) | 
| 22 | 20, 21 | eqtri 2764 | . . . 4
⊢ ∪ {suc 𝐴, suc 𝐵, suc 𝐶} = (∪ {suc 𝐴, suc 𝐵} ∪ ∪ {suc
𝐶}) | 
| 23 |  | onsuc 7832 | . . . . . . 7
⊢ ((𝐴 ∪ 𝐵) ∈ On → suc (𝐴 ∪ 𝐵) ∈ On) | 
| 24 | 1, 23 | syl 17 | . . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → suc (𝐴 ∪ 𝐵) ∈ On) | 
| 25 |  | onsuc 7832 | . . . . . 6
⊢ (𝐶 ∈ On → suc 𝐶 ∈ On) | 
| 26 |  | uniprg 4922 | . . . . . 6
⊢ ((suc
(𝐴 ∪ 𝐵) ∈ On ∧ suc 𝐶 ∈ On) → ∪ {suc (𝐴 ∪ 𝐵), suc 𝐶} = (suc (𝐴 ∪ 𝐵) ∪ suc 𝐶)) | 
| 27 | 24, 25, 26 | syl2an 596 | . . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ∪ {suc (𝐴 ∪ 𝐵), suc 𝐶} = (suc (𝐴 ∪ 𝐵) ∪ suc 𝐶)) | 
| 28 |  | suceq 6449 | . . . . . . . . 9
⊢ (∪ {𝐴,
𝐵} = (𝐴 ∪ 𝐵) → suc ∪
{𝐴, 𝐵} = suc (𝐴 ∪ 𝐵)) | 
| 29 | 4, 28 | syl 17 | . . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → suc ∪ {𝐴,
𝐵} = suc (𝐴 ∪ 𝐵)) | 
| 30 |  | onsucunipr 43390 | . . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → suc ∪ {𝐴,
𝐵} = ∪ {suc 𝐴, suc 𝐵}) | 
| 31 | 29, 30 | eqtr3d 2778 | . . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → suc (𝐴 ∪ 𝐵) = ∪ {suc 𝐴, suc 𝐵}) | 
| 32 | 31 | adantr 480 | . . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → suc (𝐴 ∪ 𝐵) = ∪ {suc 𝐴, suc 𝐵}) | 
| 33 |  | unisng 4924 | . . . . . . . . 9
⊢ (suc
𝐶 ∈ On → ∪ {suc 𝐶} = suc 𝐶) | 
| 34 | 25, 33 | syl 17 | . . . . . . . 8
⊢ (𝐶 ∈ On → ∪ {suc 𝐶} = suc 𝐶) | 
| 35 | 34 | eqcomd 2742 | . . . . . . 7
⊢ (𝐶 ∈ On → suc 𝐶 = ∪
{suc 𝐶}) | 
| 36 | 35 | adantl 481 | . . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → suc 𝐶 = ∪
{suc 𝐶}) | 
| 37 | 32, 36 | uneq12d 4168 | . . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → (suc (𝐴 ∪ 𝐵) ∪ suc 𝐶) = (∪ {suc 𝐴, suc 𝐵} ∪ ∪ {suc
𝐶})) | 
| 38 | 27, 37 | eqtrd 2776 | . . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ∪ {suc (𝐴 ∪ 𝐵), suc 𝐶} = (∪ {suc 𝐴, suc 𝐵} ∪ ∪ {suc
𝐶})) | 
| 39 | 22, 38 | eqtr4id 2795 | . . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ∪ {suc 𝐴, suc 𝐵, suc 𝐶} = ∪ {suc (𝐴 ∪ 𝐵), suc 𝐶}) | 
| 40 | 3, 18, 39 | 3eqtr4d 2786 | . 2
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → suc ∪ {𝐴,
𝐵, 𝐶} = ∪ {suc 𝐴, suc 𝐵, suc 𝐶}) | 
| 41 | 40 | 3impa 1109 | 1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → suc ∪ {𝐴,
𝐵, 𝐶} = ∪ {suc 𝐴, suc 𝐵, suc 𝐶}) |