| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | onsucsuccmpi.1 | . . . 4
⊢ 𝐴 ∈ On | 
| 2 | 1 | onsuci 7859 | . . 3
⊢ suc 𝐴 ∈ On | 
| 3 |  | onsuctop 36434 | . . 3
⊢ (suc
𝐴 ∈ On → suc suc
𝐴 ∈
Top) | 
| 4 | 2, 3 | ax-mp 5 | . 2
⊢ suc suc
𝐴 ∈
Top | 
| 5 | 1 | onirri 6497 | . . . . . . 7
⊢  ¬
𝐴 ∈ 𝐴 | 
| 6 | 1, 1 | onsucssi 7862 | . . . . . . 7
⊢ (𝐴 ∈ 𝐴 ↔ suc 𝐴 ⊆ 𝐴) | 
| 7 | 5, 6 | mtbi 322 | . . . . . 6
⊢  ¬
suc 𝐴 ⊆ 𝐴 | 
| 8 |  | sseq1 4009 | . . . . . 6
⊢ (suc
𝐴 = ∪ 𝑦
→ (suc 𝐴 ⊆ 𝐴 ↔ ∪ 𝑦
⊆ 𝐴)) | 
| 9 | 7, 8 | mtbii 326 | . . . . 5
⊢ (suc
𝐴 = ∪ 𝑦
→ ¬ ∪ 𝑦 ⊆ 𝐴) | 
| 10 |  | elpwi 4607 | . . . . . . 7
⊢ (𝑦 ∈ 𝒫 suc 𝐴 → 𝑦 ⊆ suc 𝐴) | 
| 11 | 10 | unissd 4917 | . . . . . 6
⊢ (𝑦 ∈ 𝒫 suc 𝐴 → ∪ 𝑦
⊆ ∪ suc 𝐴) | 
| 12 | 1 | onunisuci 6504 | . . . . . 6
⊢ ∪ suc 𝐴 = 𝐴 | 
| 13 | 11, 12 | sseqtrdi 4024 | . . . . 5
⊢ (𝑦 ∈ 𝒫 suc 𝐴 → ∪ 𝑦
⊆ 𝐴) | 
| 14 | 9, 13 | nsyl 140 | . . . 4
⊢ (suc
𝐴 = ∪ 𝑦
→ ¬ 𝑦 ∈
𝒫 suc 𝐴) | 
| 15 |  | eldif 3961 | . . . . . . 7
⊢ (𝑦 ∈ (𝒫 (suc 𝐴 ∪ {suc 𝐴}) ∖ 𝒫 suc 𝐴) ↔ (𝑦 ∈ 𝒫 (suc 𝐴 ∪ {suc 𝐴}) ∧ ¬ 𝑦 ∈ 𝒫 suc 𝐴)) | 
| 16 |  | elpwunsn 4684 | . . . . . . 7
⊢ (𝑦 ∈ (𝒫 (suc 𝐴 ∪ {suc 𝐴}) ∖ 𝒫 suc 𝐴) → suc 𝐴 ∈ 𝑦) | 
| 17 | 15, 16 | sylbir 235 | . . . . . 6
⊢ ((𝑦 ∈ 𝒫 (suc 𝐴 ∪ {suc 𝐴}) ∧ ¬ 𝑦 ∈ 𝒫 suc 𝐴) → suc 𝐴 ∈ 𝑦) | 
| 18 | 17 | ex 412 | . . . . 5
⊢ (𝑦 ∈ 𝒫 (suc 𝐴 ∪ {suc 𝐴}) → (¬ 𝑦 ∈ 𝒫 suc 𝐴 → suc 𝐴 ∈ 𝑦)) | 
| 19 |  | df-suc 6390 | . . . . . 6
⊢ suc suc
𝐴 = (suc 𝐴 ∪ {suc 𝐴}) | 
| 20 | 19 | pweqi 4616 | . . . . 5
⊢ 𝒫
suc suc 𝐴 = 𝒫 (suc
𝐴 ∪ {suc 𝐴}) | 
| 21 | 18, 20 | eleq2s 2859 | . . . 4
⊢ (𝑦 ∈ 𝒫 suc suc 𝐴 → (¬ 𝑦 ∈ 𝒫 suc 𝐴 → suc 𝐴 ∈ 𝑦)) | 
| 22 |  | snelpwi 5448 | . . . . 5
⊢ (suc
𝐴 ∈ 𝑦 → {suc 𝐴} ∈ 𝒫 𝑦) | 
| 23 |  | snfi 9083 | . . . . . . . 8
⊢ {suc
𝐴} ∈
Fin | 
| 24 | 23 | jctr 524 | . . . . . . 7
⊢ ({suc
𝐴} ∈ 𝒫 𝑦 → ({suc 𝐴} ∈ 𝒫 𝑦 ∧ {suc 𝐴} ∈ Fin)) | 
| 25 |  | elin 3967 | . . . . . . 7
⊢ ({suc
𝐴} ∈ (𝒫 𝑦 ∩ Fin) ↔ ({suc 𝐴} ∈ 𝒫 𝑦 ∧ {suc 𝐴} ∈ Fin)) | 
| 26 | 24, 25 | sylibr 234 | . . . . . 6
⊢ ({suc
𝐴} ∈ 𝒫 𝑦 → {suc 𝐴} ∈ (𝒫 𝑦 ∩ Fin)) | 
| 27 | 2 | elexi 3503 | . . . . . . . 8
⊢ suc 𝐴 ∈ V | 
| 28 | 27 | unisn 4926 | . . . . . . 7
⊢ ∪ {suc 𝐴} = suc 𝐴 | 
| 29 | 28 | eqcomi 2746 | . . . . . 6
⊢ suc 𝐴 = ∪
{suc 𝐴} | 
| 30 |  | unieq 4918 | . . . . . . 7
⊢ (𝑧 = {suc 𝐴} → ∪ 𝑧 = ∪
{suc 𝐴}) | 
| 31 | 30 | rspceeqv 3645 | . . . . . 6
⊢ (({suc
𝐴} ∈ (𝒫 𝑦 ∩ Fin) ∧ suc 𝐴 = ∪
{suc 𝐴}) →
∃𝑧 ∈ (𝒫
𝑦 ∩ Fin)suc 𝐴 = ∪
𝑧) | 
| 32 | 26, 29, 31 | sylancl 586 | . . . . 5
⊢ ({suc
𝐴} ∈ 𝒫 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)suc 𝐴 = ∪ 𝑧) | 
| 33 | 22, 32 | syl 17 | . . . 4
⊢ (suc
𝐴 ∈ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)suc 𝐴 = ∪ 𝑧) | 
| 34 | 14, 21, 33 | syl56 36 | . . 3
⊢ (𝑦 ∈ 𝒫 suc suc 𝐴 → (suc 𝐴 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)suc 𝐴 = ∪ 𝑧)) | 
| 35 | 34 | rgen 3063 | . 2
⊢
∀𝑦 ∈
𝒫 suc suc 𝐴(suc
𝐴 = ∪ 𝑦
→ ∃𝑧 ∈
(𝒫 𝑦 ∩ Fin)suc
𝐴 = ∪ 𝑧) | 
| 36 | 2 | onunisuci 6504 | . . . 4
⊢ ∪ suc suc 𝐴 = suc 𝐴 | 
| 37 | 36 | eqcomi 2746 | . . 3
⊢ suc 𝐴 = ∪
suc suc 𝐴 | 
| 38 | 37 | iscmp 23396 | . 2
⊢ (suc suc
𝐴 ∈ Comp ↔ (suc
suc 𝐴 ∈ Top ∧
∀𝑦 ∈ 𝒫
suc suc 𝐴(suc 𝐴 = ∪
𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)suc 𝐴 = ∪ 𝑧))) | 
| 39 | 4, 35, 38 | mpbir2an 711 | 1
⊢ suc suc
𝐴 ∈
Comp |