Step | Hyp | Ref
| Expression |
1 | | distop 21605 |
. . . 4
⊢ (𝐴 ∈ Fin → 𝒫
𝐴 ∈
Top) |
2 | | pwfi 8821 |
. . . . 5
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
3 | 2 | biimpi 218 |
. . . 4
⊢ (𝐴 ∈ Fin → 𝒫
𝐴 ∈
Fin) |
4 | 1, 3 | elind 4173 |
. . 3
⊢ (𝐴 ∈ Fin → 𝒫
𝐴 ∈ (Top ∩
Fin)) |
5 | | fincmp 22003 |
. . 3
⊢
(𝒫 𝐴 ∈
(Top ∩ Fin) → 𝒫 𝐴 ∈ Comp) |
6 | 4, 5 | syl 17 |
. 2
⊢ (𝐴 ∈ Fin → 𝒫
𝐴 ∈
Comp) |
7 | | simpr 487 |
. . . . . . . 8
⊢
((𝒫 𝐴 ∈
Comp ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
8 | 7 | snssd 4744 |
. . . . . . 7
⊢
((𝒫 𝐴 ∈
Comp ∧ 𝑥 ∈ 𝐴) → {𝑥} ⊆ 𝐴) |
9 | | snex 5334 |
. . . . . . . 8
⊢ {𝑥} ∈ V |
10 | 9 | elpw 4545 |
. . . . . . 7
⊢ ({𝑥} ∈ 𝒫 𝐴 ↔ {𝑥} ⊆ 𝐴) |
11 | 8, 10 | sylibr 236 |
. . . . . 6
⊢
((𝒫 𝐴 ∈
Comp ∧ 𝑥 ∈ 𝐴) → {𝑥} ∈ 𝒫 𝐴) |
12 | 11 | fmpttd 6881 |
. . . . 5
⊢
(𝒫 𝐴 ∈
Comp → (𝑥 ∈ 𝐴 ↦ {𝑥}):𝐴⟶𝒫 𝐴) |
13 | 12 | frnd 6523 |
. . . 4
⊢
(𝒫 𝐴 ∈
Comp → ran (𝑥 ∈
𝐴 ↦ {𝑥}) ⊆ 𝒫 𝐴) |
14 | | eqid 2823 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↦ {𝑥}) = (𝑥 ∈ 𝐴 ↦ {𝑥}) |
15 | 14 | rnmpt 5829 |
. . . . . . 7
⊢ ran
(𝑥 ∈ 𝐴 ↦ {𝑥}) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} |
16 | 15 | unieqi 4853 |
. . . . . 6
⊢ ∪ ran (𝑥 ∈ 𝐴 ↦ {𝑥}) = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} |
17 | 9 | dfiun2 4960 |
. . . . . 6
⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} |
18 | | iunid 4986 |
. . . . . 6
⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴 |
19 | 16, 17, 18 | 3eqtr2ri 2853 |
. . . . 5
⊢ 𝐴 = ∪
ran (𝑥 ∈ 𝐴 ↦ {𝑥}) |
20 | 19 | a1i 11 |
. . . 4
⊢
(𝒫 𝐴 ∈
Comp → 𝐴 = ∪ ran (𝑥 ∈ 𝐴 ↦ {𝑥})) |
21 | | unipw 5345 |
. . . . . 6
⊢ ∪ 𝒫 𝐴 = 𝐴 |
22 | 21 | eqcomi 2832 |
. . . . 5
⊢ 𝐴 = ∪
𝒫 𝐴 |
23 | 22 | cmpcov 21999 |
. . . 4
⊢
((𝒫 𝐴 ∈
Comp ∧ ran (𝑥 ∈
𝐴 ↦ {𝑥}) ⊆ 𝒫 𝐴 ∧ 𝐴 = ∪ ran (𝑥 ∈ 𝐴 ↦ {𝑥})) → ∃𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin)𝐴 = ∪ 𝑦) |
24 | 13, 20, 23 | mpd3an23 1459 |
. . 3
⊢
(𝒫 𝐴 ∈
Comp → ∃𝑦 ∈
(𝒫 ran (𝑥 ∈
𝐴 ↦ {𝑥}) ∩ Fin)𝐴 = ∪ 𝑦) |
25 | | elinel2 4175 |
. . . . . 6
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → 𝑦 ∈ Fin) |
26 | | elinel1 4174 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → 𝑦 ∈ 𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥})) |
27 | 26 | elpwid 4552 |
. . . . . . 7
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → 𝑦 ⊆ ran (𝑥 ∈ 𝐴 ↦ {𝑥})) |
28 | | snfi 8596 |
. . . . . . . . . 10
⊢ {𝑥} ∈ Fin |
29 | 28 | rgenw 3152 |
. . . . . . . . 9
⊢
∀𝑥 ∈
𝐴 {𝑥} ∈ Fin |
30 | 14 | fmpt 6876 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐴 {𝑥} ∈ Fin ↔ (𝑥 ∈ 𝐴 ↦ {𝑥}):𝐴⟶Fin) |
31 | 29, 30 | mpbi 232 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↦ {𝑥}):𝐴⟶Fin |
32 | | frn 6522 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ↦ {𝑥}):𝐴⟶Fin → ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ⊆ Fin) |
33 | 31, 32 | mp1i 13 |
. . . . . . 7
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ⊆ Fin) |
34 | 27, 33 | sstrd 3979 |
. . . . . 6
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → 𝑦 ⊆ Fin) |
35 | | unifi 8815 |
. . . . . 6
⊢ ((𝑦 ∈ Fin ∧ 𝑦 ⊆ Fin) → ∪ 𝑦
∈ Fin) |
36 | 25, 34, 35 | syl2anc 586 |
. . . . 5
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → ∪ 𝑦
∈ Fin) |
37 | | eleq1 2902 |
. . . . 5
⊢ (𝐴 = ∪
𝑦 → (𝐴 ∈ Fin ↔ ∪ 𝑦
∈ Fin)) |
38 | 36, 37 | syl5ibrcom 249 |
. . . 4
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → (𝐴 = ∪ 𝑦 → 𝐴 ∈ Fin)) |
39 | 38 | rexlimiv 3282 |
. . 3
⊢
(∃𝑦 ∈
(𝒫 ran (𝑥 ∈
𝐴 ↦ {𝑥}) ∩ Fin)𝐴 = ∪ 𝑦 → 𝐴 ∈ Fin) |
40 | 24, 39 | syl 17 |
. 2
⊢
(𝒫 𝐴 ∈
Comp → 𝐴 ∈
Fin) |
41 | 6, 40 | impbii 211 |
1
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Comp) |