| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | distop 23002 | . . . 4
⊢ (𝐴 ∈ Fin → 𝒫
𝐴 ∈
Top) | 
| 2 |  | pwfi 9357 | . . . . 5
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) | 
| 3 | 2 | biimpi 216 | . . . 4
⊢ (𝐴 ∈ Fin → 𝒫
𝐴 ∈
Fin) | 
| 4 | 1, 3 | elind 4200 | . . 3
⊢ (𝐴 ∈ Fin → 𝒫
𝐴 ∈ (Top ∩
Fin)) | 
| 5 |  | fincmp 23401 | . . 3
⊢
(𝒫 𝐴 ∈
(Top ∩ Fin) → 𝒫 𝐴 ∈ Comp) | 
| 6 | 4, 5 | syl 17 | . 2
⊢ (𝐴 ∈ Fin → 𝒫
𝐴 ∈
Comp) | 
| 7 |  | simpr 484 | . . . . . . . 8
⊢
((𝒫 𝐴 ∈
Comp ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) | 
| 8 | 7 | snssd 4809 | . . . . . . 7
⊢
((𝒫 𝐴 ∈
Comp ∧ 𝑥 ∈ 𝐴) → {𝑥} ⊆ 𝐴) | 
| 9 |  | vsnex 5434 | . . . . . . . 8
⊢ {𝑥} ∈ V | 
| 10 | 9 | elpw 4604 | . . . . . . 7
⊢ ({𝑥} ∈ 𝒫 𝐴 ↔ {𝑥} ⊆ 𝐴) | 
| 11 | 8, 10 | sylibr 234 | . . . . . 6
⊢
((𝒫 𝐴 ∈
Comp ∧ 𝑥 ∈ 𝐴) → {𝑥} ∈ 𝒫 𝐴) | 
| 12 | 11 | fmpttd 7135 | . . . . 5
⊢
(𝒫 𝐴 ∈
Comp → (𝑥 ∈ 𝐴 ↦ {𝑥}):𝐴⟶𝒫 𝐴) | 
| 13 | 12 | frnd 6744 | . . . 4
⊢
(𝒫 𝐴 ∈
Comp → ran (𝑥 ∈
𝐴 ↦ {𝑥}) ⊆ 𝒫 𝐴) | 
| 14 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↦ {𝑥}) = (𝑥 ∈ 𝐴 ↦ {𝑥}) | 
| 15 | 14 | rnmpt 5968 | . . . . . . 7
⊢ ran
(𝑥 ∈ 𝐴 ↦ {𝑥}) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} | 
| 16 | 15 | unieqi 4919 | . . . . . 6
⊢ ∪ ran (𝑥 ∈ 𝐴 ↦ {𝑥}) = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} | 
| 17 | 9 | dfiun2 5033 | . . . . . 6
⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} | 
| 18 |  | iunid 5060 | . . . . . 6
⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴 | 
| 19 | 16, 17, 18 | 3eqtr2ri 2772 | . . . . 5
⊢ 𝐴 = ∪
ran (𝑥 ∈ 𝐴 ↦ {𝑥}) | 
| 20 | 19 | a1i 11 | . . . 4
⊢
(𝒫 𝐴 ∈
Comp → 𝐴 = ∪ ran (𝑥 ∈ 𝐴 ↦ {𝑥})) | 
| 21 |  | unipw 5455 | . . . . . 6
⊢ ∪ 𝒫 𝐴 = 𝐴 | 
| 22 | 21 | eqcomi 2746 | . . . . 5
⊢ 𝐴 = ∪
𝒫 𝐴 | 
| 23 | 22 | cmpcov 23397 | . . . 4
⊢
((𝒫 𝐴 ∈
Comp ∧ ran (𝑥 ∈
𝐴 ↦ {𝑥}) ⊆ 𝒫 𝐴 ∧ 𝐴 = ∪ ran (𝑥 ∈ 𝐴 ↦ {𝑥})) → ∃𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin)𝐴 = ∪ 𝑦) | 
| 24 | 13, 20, 23 | mpd3an23 1465 | . . 3
⊢
(𝒫 𝐴 ∈
Comp → ∃𝑦 ∈
(𝒫 ran (𝑥 ∈
𝐴 ↦ {𝑥}) ∩ Fin)𝐴 = ∪ 𝑦) | 
| 25 |  | elinel2 4202 | . . . . . 6
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → 𝑦 ∈ Fin) | 
| 26 |  | elinel1 4201 | . . . . . . . 8
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → 𝑦 ∈ 𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥})) | 
| 27 | 26 | elpwid 4609 | . . . . . . 7
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → 𝑦 ⊆ ran (𝑥 ∈ 𝐴 ↦ {𝑥})) | 
| 28 |  | snfi 9083 | . . . . . . . . . 10
⊢ {𝑥} ∈ Fin | 
| 29 | 28 | rgenw 3065 | . . . . . . . . 9
⊢
∀𝑥 ∈
𝐴 {𝑥} ∈ Fin | 
| 30 | 14 | fmpt 7130 | . . . . . . . . 9
⊢
(∀𝑥 ∈
𝐴 {𝑥} ∈ Fin ↔ (𝑥 ∈ 𝐴 ↦ {𝑥}):𝐴⟶Fin) | 
| 31 | 29, 30 | mpbi 230 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↦ {𝑥}):𝐴⟶Fin | 
| 32 |  | frn 6743 | . . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ↦ {𝑥}):𝐴⟶Fin → ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ⊆ Fin) | 
| 33 | 31, 32 | mp1i 13 | . . . . . . 7
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ⊆ Fin) | 
| 34 | 27, 33 | sstrd 3994 | . . . . . 6
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → 𝑦 ⊆ Fin) | 
| 35 |  | unifi 9384 | . . . . . 6
⊢ ((𝑦 ∈ Fin ∧ 𝑦 ⊆ Fin) → ∪ 𝑦
∈ Fin) | 
| 36 | 25, 34, 35 | syl2anc 584 | . . . . 5
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → ∪ 𝑦
∈ Fin) | 
| 37 |  | eleq1 2829 | . . . . 5
⊢ (𝐴 = ∪
𝑦 → (𝐴 ∈ Fin ↔ ∪ 𝑦
∈ Fin)) | 
| 38 | 36, 37 | syl5ibrcom 247 | . . . 4
⊢ (𝑦 ∈ (𝒫 ran (𝑥 ∈ 𝐴 ↦ {𝑥}) ∩ Fin) → (𝐴 = ∪ 𝑦 → 𝐴 ∈ Fin)) | 
| 39 | 38 | rexlimiv 3148 | . . 3
⊢
(∃𝑦 ∈
(𝒫 ran (𝑥 ∈
𝐴 ↦ {𝑥}) ∩ Fin)𝐴 = ∪ 𝑦 → 𝐴 ∈ Fin) | 
| 40 | 24, 39 | syl 17 | . 2
⊢
(𝒫 𝐴 ∈
Comp → 𝐴 ∈
Fin) | 
| 41 | 6, 40 | impbii 209 | 1
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Comp) |