Step | Hyp | Ref
| Expression |
1 | | distop 20610 |
. . . 4
⊢ (𝐴 ∈ Fin → 𝒫
𝐴 ∈
Top) |
2 | | pwfi 8144 |
. . . . 5
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
3 | 2 | biimpi 205 |
. . . 4
⊢ (𝐴 ∈ Fin → 𝒫
𝐴 ∈
Fin) |
4 | 1, 3 | elind 3760 |
. . 3
⊢ (𝐴 ∈ Fin → 𝒫
𝐴 ∈ (Top ∩
Fin)) |
5 | | fincmp 21006 |
. . 3
⊢
(𝒫 𝐴 ∈
(Top ∩ Fin) → 𝒫 𝐴 ∈ Comp) |
6 | 4, 5 | syl 17 |
. 2
⊢ (𝐴 ∈ Fin → 𝒫
𝐴 ∈
Comp) |
7 | | simpr 476 |
. . . . . . . 8
⊢
((𝒫 𝐴 ∈
Comp ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
8 | 7 | snssd 4281 |
. . . . . . 7
⊢
((𝒫 𝐴 ∈
Comp ∧ 𝑥 ∈ 𝐴) → {𝑥} ⊆ 𝐴) |
9 | | snex 4835 |
. . . . . . . 8
⊢ {𝑥} ∈ V |
10 | 9 | elpw 4114 |
. . . . . . 7
⊢ ({𝑥} ∈ 𝒫 𝐴 ↔ {𝑥} ⊆ 𝐴) |
11 | 8, 10 | sylibr 223 |
. . . . . 6
⊢
((𝒫 𝐴 ∈
Comp ∧ 𝑥 ∈ 𝐴) → {𝑥} ∈ 𝒫 𝐴) |
12 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↦ {𝑥}) = (𝑥 ∈ 𝐴 ↦ {𝑥}) |
13 | 11, 12 | fmptd 6292 |
. . . . 5
⊢
(𝒫 𝐴 ∈
Comp → (𝑥 ∈ 𝐴 ↦ {𝑥}):𝐴⟶𝒫 𝐴) |
14 | | frn 5966 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ↦ {𝑥}):𝐴⟶𝒫 𝐴 → ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ⊆ 𝒫 𝐴) |
15 | 13, 14 | syl 17 |
. . . 4
⊢
(𝒫 𝐴 ∈
Comp → ran (𝑥 ∈
𝐴 ↦ {𝑥}) ⊆ 𝒫 𝐴) |
16 | 12 | rnmpt 5292 |
. . . . . . 7
⊢ ran
(𝑥 ∈ 𝐴 ↦ {𝑥}) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} |
17 | 16 | unieqi 4381 |
. . . . . 6
⊢ ∪ ran (𝑥 ∈ 𝐴 ↦ {𝑥}) = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} |
18 | 9 | dfiun2 4490 |
. . . . . 6
⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} |
19 | | iunid 4511 |
. . . . . 6
⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴 |
20 | 17, 18, 19 | 3eqtr2ri 2639 |
. . . . 5
⊢ 𝐴 = ∪
ran (𝑥 ∈ 𝐴 ↦ {𝑥}) |
21 | 20 | a1i 11 |
. . . 4
⊢
(𝒫 𝐴 ∈
Comp → 𝐴 = ∪ ran (𝑥 ∈ 𝐴 ↦ {𝑥})) |
22 | | unipw 4845 |
. . . . . 6
⊢ ∪ 𝒫 𝐴 = 𝐴 |
23 | 22 | eqcomi 2619 |
. . . . 5
⊢ 𝐴 = ∪
𝒫 𝐴 |
24 | 23 | cmpcov 21002 |
. . . 4
⊢
((𝒫 𝐴 ∈
Comp ∧ ran (𝑥 ∈
𝐴 ↦ {𝑥}) ⊆ 𝒫 𝐴 ∧ 𝐴 = ∪ ran (𝑥 ∈ 𝐴 ↦ {𝑥})) → ∃𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin)𝐴 = ∪ 𝑦) |
25 | 15, 21, 24 | mpd3an23 1418 |
. . 3
⊢
(𝒫 𝐴 ∈
Comp → ∃𝑦 ∈
(𝒫 ran (𝑥 ∈
𝐴 ↦ {𝑥}) ∩ Fin)𝐴 = ∪ 𝑦) |
26 | | elin 3758 |
. . . . . . 7
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) ↔ (𝑦 ∈ 𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∧ 𝑦 ∈ Fin)) |
27 | 26 | simprbi 479 |
. . . . . 6
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → 𝑦 ∈ Fin) |
28 | 26 | simplbi 475 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → 𝑦 ∈ 𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥})) |
29 | 28 | elpwid 4118 |
. . . . . . 7
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → 𝑦 ⊆ ran (𝑥 ∈ 𝐴 ↦ {𝑥})) |
30 | | snfi 7923 |
. . . . . . . . . 10
⊢ {𝑥} ∈ Fin |
31 | 30 | rgenw 2908 |
. . . . . . . . 9
⊢
∀𝑥 ∈
𝐴 {𝑥} ∈ Fin |
32 | 12 | fmpt 6289 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐴 {𝑥} ∈ Fin ↔ (𝑥 ∈ 𝐴 ↦ {𝑥}):𝐴⟶Fin) |
33 | 31, 32 | mpbi 219 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↦ {𝑥}):𝐴⟶Fin |
34 | | frn 5966 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ↦ {𝑥}):𝐴⟶Fin → ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ⊆ Fin) |
35 | 33, 34 | mp1i 13 |
. . . . . . 7
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ⊆ Fin) |
36 | 29, 35 | sstrd 3578 |
. . . . . 6
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → 𝑦 ⊆ Fin) |
37 | | unifi 8138 |
. . . . . 6
⊢ ((𝑦 ∈ Fin ∧ 𝑦 ⊆ Fin) → ∪ 𝑦
∈ Fin) |
38 | 27, 36, 37 | syl2anc 691 |
. . . . 5
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → ∪ 𝑦
∈ Fin) |
39 | | eleq1 2676 |
. . . . 5
⊢ (𝐴 = ∪
𝑦 → (𝐴 ∈ Fin ↔ ∪ 𝑦
∈ Fin)) |
40 | 38, 39 | syl5ibrcom 236 |
. . . 4
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → (𝐴 = ∪ 𝑦 → 𝐴 ∈ Fin)) |
41 | 40 | rexlimiv 3009 |
. . 3
⊢
(∃𝑦 ∈
(𝒫 ran (𝑥 ∈
𝐴 ↦ {𝑥}) ∩ Fin)𝐴 = ∪ 𝑦 → 𝐴 ∈ Fin) |
42 | 25, 41 | syl 17 |
. 2
⊢
(𝒫 𝐴 ∈
Comp → 𝐴 ∈
Fin) |
43 | 6, 42 | impbii 198 |
1
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Comp) |