Proof of Theorem onsucuni2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eleq1 2828 | . . . . . 6
⊢ (𝐴 = suc 𝐵 → (𝐴 ∈ On ↔ suc 𝐵 ∈ On)) | 
| 2 | 1 | biimpac 478 | . . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐴 = suc 𝐵) → suc 𝐵 ∈ On) | 
| 3 |  | eloni 6393 | . . . . 5
⊢ (suc
𝐵 ∈ On → Ord suc
𝐵) | 
| 4 |  | ordsuc 7834 | . . . . . . . 8
⊢ (Ord
𝐵 ↔ Ord suc 𝐵) | 
| 5 |  | ordunisuc 7853 | . . . . . . . 8
⊢ (Ord
𝐵 → ∪ suc 𝐵 = 𝐵) | 
| 6 | 4, 5 | sylbir 235 | . . . . . . 7
⊢ (Ord suc
𝐵 → ∪ suc 𝐵 = 𝐵) | 
| 7 |  | suceq 6449 | . . . . . . 7
⊢ (∪ suc 𝐵 = 𝐵 → suc ∪ suc
𝐵 = suc 𝐵) | 
| 8 | 6, 7 | syl 17 | . . . . . 6
⊢ (Ord suc
𝐵 → suc ∪ suc 𝐵 = suc 𝐵) | 
| 9 |  | ordunisuc 7853 | . . . . . 6
⊢ (Ord suc
𝐵 → ∪ suc suc 𝐵 = suc 𝐵) | 
| 10 | 8, 9 | eqtr4d 2779 | . . . . 5
⊢ (Ord suc
𝐵 → suc ∪ suc 𝐵 = ∪ suc suc
𝐵) | 
| 11 | 2, 3, 10 | 3syl 18 | . . . 4
⊢ ((𝐴 ∈ On ∧ 𝐴 = suc 𝐵) → suc ∪
suc 𝐵 = ∪ suc suc 𝐵) | 
| 12 |  | unieq 4917 | . . . . . 6
⊢ (𝐴 = suc 𝐵 → ∪ 𝐴 = ∪
suc 𝐵) | 
| 13 |  | suceq 6449 | . . . . . 6
⊢ (∪ 𝐴 =
∪ suc 𝐵 → suc ∪
𝐴 = suc ∪ suc 𝐵) | 
| 14 | 12, 13 | syl 17 | . . . . 5
⊢ (𝐴 = suc 𝐵 → suc ∪
𝐴 = suc ∪ suc 𝐵) | 
| 15 |  | suceq 6449 | . . . . . 6
⊢ (𝐴 = suc 𝐵 → suc 𝐴 = suc suc 𝐵) | 
| 16 | 15 | unieqd 4919 | . . . . 5
⊢ (𝐴 = suc 𝐵 → ∪ suc
𝐴 = ∪ suc suc 𝐵) | 
| 17 | 14, 16 | eqeq12d 2752 | . . . 4
⊢ (𝐴 = suc 𝐵 → (suc ∪
𝐴 = ∪ suc 𝐴 ↔ suc ∪ suc
𝐵 = ∪ suc suc 𝐵)) | 
| 18 | 11, 17 | imbitrrid 246 | . . 3
⊢ (𝐴 = suc 𝐵 → ((𝐴 ∈ On ∧ 𝐴 = suc 𝐵) → suc ∪
𝐴 = ∪ suc 𝐴)) | 
| 19 | 18 | anabsi7 671 | . 2
⊢ ((𝐴 ∈ On ∧ 𝐴 = suc 𝐵) → suc ∪
𝐴 = ∪ suc 𝐴) | 
| 20 |  | eloni 6393 | . . . 4
⊢ (𝐴 ∈ On → Ord 𝐴) | 
| 21 |  | ordunisuc 7853 | . . . 4
⊢ (Ord
𝐴 → ∪ suc 𝐴 = 𝐴) | 
| 22 | 20, 21 | syl 17 | . . 3
⊢ (𝐴 ∈ On → ∪ suc 𝐴 = 𝐴) | 
| 23 | 22 | adantr 480 | . 2
⊢ ((𝐴 ∈ On ∧ 𝐴 = suc 𝐵) → ∪ suc
𝐴 = 𝐴) | 
| 24 | 19, 23 | eqtrd 2776 | 1
⊢ ((𝐴 ∈ On ∧ 𝐴 = suc 𝐵) → suc ∪
𝐴 = 𝐴) |