Step | Hyp | Ref
| Expression |
1 | | onsucsuccmpi.1 |
. . . 4
⊢ 𝐴 ∈ On |
2 | 1 | onsuci 7038 |
. . 3
⊢ suc 𝐴 ∈ On |
3 | | onsuctop 32432 |
. . 3
⊢ (suc
𝐴 ∈ On → suc suc
𝐴 ∈
Top) |
4 | 2, 3 | ax-mp 5 |
. 2
⊢ suc suc
𝐴 ∈
Top |
5 | 1 | onirri 5834 |
. . . . . . 7
⊢ ¬
𝐴 ∈ 𝐴 |
6 | 1, 1 | onsucssi 7041 |
. . . . . . 7
⊢ (𝐴 ∈ 𝐴 ↔ suc 𝐴 ⊆ 𝐴) |
7 | 5, 6 | mtbi 312 |
. . . . . 6
⊢ ¬
suc 𝐴 ⊆ 𝐴 |
8 | | sseq1 3626 |
. . . . . 6
⊢ (suc
𝐴 = ∪ 𝑦
→ (suc 𝐴 ⊆ 𝐴 ↔ ∪ 𝑦
⊆ 𝐴)) |
9 | 7, 8 | mtbii 316 |
. . . . 5
⊢ (suc
𝐴 = ∪ 𝑦
→ ¬ ∪ 𝑦 ⊆ 𝐴) |
10 | | elpwi 4168 |
. . . . . . 7
⊢ (𝑦 ∈ 𝒫 suc 𝐴 → 𝑦 ⊆ suc 𝐴) |
11 | 10 | unissd 4462 |
. . . . . 6
⊢ (𝑦 ∈ 𝒫 suc 𝐴 → ∪ 𝑦
⊆ ∪ suc 𝐴) |
12 | 1 | onunisuci 5841 |
. . . . . 6
⊢ ∪ suc 𝐴 = 𝐴 |
13 | 11, 12 | syl6sseq 3651 |
. . . . 5
⊢ (𝑦 ∈ 𝒫 suc 𝐴 → ∪ 𝑦
⊆ 𝐴) |
14 | 9, 13 | nsyl 135 |
. . . 4
⊢ (suc
𝐴 = ∪ 𝑦
→ ¬ 𝑦 ∈
𝒫 suc 𝐴) |
15 | | eldif 3584 |
. . . . . . 7
⊢ (𝑦 ∈ (𝒫 (suc 𝐴 ∪ {suc 𝐴}) ∖ 𝒫 suc 𝐴) ↔ (𝑦 ∈ 𝒫 (suc 𝐴 ∪ {suc 𝐴}) ∧ ¬ 𝑦 ∈ 𝒫 suc 𝐴)) |
16 | | elpwunsn 4224 |
. . . . . . 7
⊢ (𝑦 ∈ (𝒫 (suc 𝐴 ∪ {suc 𝐴}) ∖ 𝒫 suc 𝐴) → suc 𝐴 ∈ 𝑦) |
17 | 15, 16 | sylbir 225 |
. . . . . 6
⊢ ((𝑦 ∈ 𝒫 (suc 𝐴 ∪ {suc 𝐴}) ∧ ¬ 𝑦 ∈ 𝒫 suc 𝐴) → suc 𝐴 ∈ 𝑦) |
18 | 17 | ex 450 |
. . . . 5
⊢ (𝑦 ∈ 𝒫 (suc 𝐴 ∪ {suc 𝐴}) → (¬ 𝑦 ∈ 𝒫 suc 𝐴 → suc 𝐴 ∈ 𝑦)) |
19 | | df-suc 5729 |
. . . . . 6
⊢ suc suc
𝐴 = (suc 𝐴 ∪ {suc 𝐴}) |
20 | 19 | pweqi 4162 |
. . . . 5
⊢ 𝒫
suc suc 𝐴 = 𝒫 (suc
𝐴 ∪ {suc 𝐴}) |
21 | 18, 20 | eleq2s 2719 |
. . . 4
⊢ (𝑦 ∈ 𝒫 suc suc 𝐴 → (¬ 𝑦 ∈ 𝒫 suc 𝐴 → suc 𝐴 ∈ 𝑦)) |
22 | | snelpwi 4912 |
. . . . 5
⊢ (suc
𝐴 ∈ 𝑦 → {suc 𝐴} ∈ 𝒫 𝑦) |
23 | | snfi 8038 |
. . . . . . . 8
⊢ {suc
𝐴} ∈
Fin |
24 | 23 | jctr 565 |
. . . . . . 7
⊢ ({suc
𝐴} ∈ 𝒫 𝑦 → ({suc 𝐴} ∈ 𝒫 𝑦 ∧ {suc 𝐴} ∈ Fin)) |
25 | | elin 3796 |
. . . . . . 7
⊢ ({suc
𝐴} ∈ (𝒫 𝑦 ∩ Fin) ↔ ({suc 𝐴} ∈ 𝒫 𝑦 ∧ {suc 𝐴} ∈ Fin)) |
26 | 24, 25 | sylibr 224 |
. . . . . 6
⊢ ({suc
𝐴} ∈ 𝒫 𝑦 → {suc 𝐴} ∈ (𝒫 𝑦 ∩ Fin)) |
27 | 2 | elexi 3213 |
. . . . . . . 8
⊢ suc 𝐴 ∈ V |
28 | 27 | unisn 4451 |
. . . . . . 7
⊢ ∪ {suc 𝐴} = suc 𝐴 |
29 | 28 | eqcomi 2631 |
. . . . . 6
⊢ suc 𝐴 = ∪
{suc 𝐴} |
30 | | unieq 4444 |
. . . . . . . 8
⊢ (𝑧 = {suc 𝐴} → ∪ 𝑧 = ∪
{suc 𝐴}) |
31 | 30 | eqeq2d 2632 |
. . . . . . 7
⊢ (𝑧 = {suc 𝐴} → (suc 𝐴 = ∪ 𝑧 ↔ suc 𝐴 = ∪ {suc 𝐴})) |
32 | 31 | rspcev 3309 |
. . . . . 6
⊢ (({suc
𝐴} ∈ (𝒫 𝑦 ∩ Fin) ∧ suc 𝐴 = ∪
{suc 𝐴}) →
∃𝑧 ∈ (𝒫
𝑦 ∩ Fin)suc 𝐴 = ∪
𝑧) |
33 | 26, 29, 32 | sylancl 694 |
. . . . 5
⊢ ({suc
𝐴} ∈ 𝒫 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)suc 𝐴 = ∪ 𝑧) |
34 | 22, 33 | syl 17 |
. . . 4
⊢ (suc
𝐴 ∈ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)suc 𝐴 = ∪ 𝑧) |
35 | 14, 21, 34 | syl56 36 |
. . 3
⊢ (𝑦 ∈ 𝒫 suc suc 𝐴 → (suc 𝐴 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)suc 𝐴 = ∪ 𝑧)) |
36 | 35 | rgen 2922 |
. 2
⊢
∀𝑦 ∈
𝒫 suc suc 𝐴(suc
𝐴 = ∪ 𝑦
→ ∃𝑧 ∈
(𝒫 𝑦 ∩ Fin)suc
𝐴 = ∪ 𝑧) |
37 | 2 | onunisuci 5841 |
. . . 4
⊢ ∪ suc suc 𝐴 = suc 𝐴 |
38 | 37 | eqcomi 2631 |
. . 3
⊢ suc 𝐴 = ∪
suc suc 𝐴 |
39 | 38 | iscmp 21191 |
. 2
⊢ (suc suc
𝐴 ∈ Comp ↔ (suc
suc 𝐴 ∈ Top ∧
∀𝑦 ∈ 𝒫
suc suc 𝐴(suc 𝐴 = ∪
𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)suc 𝐴 = ∪ 𝑧))) |
40 | 4, 36, 39 | mpbir2an 955 |
1
⊢ suc suc
𝐴 ∈
Comp |