| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lfinpfin 23533 | . . 3
⊢ (𝐶 ∈ (LocFin‘𝒫
𝑋) → 𝐶 ∈ PtFin) | 
| 2 |  | unipw 5454 | . . . . 5
⊢ ∪ 𝒫 𝑋 = 𝑋 | 
| 3 | 2 | eqcomi 2745 | . . . 4
⊢ 𝑋 = ∪
𝒫 𝑋 | 
| 4 |  | locfindis.1 | . . . 4
⊢ 𝑌 = ∪
𝐶 | 
| 5 | 3, 4 | locfinbas 23531 | . . 3
⊢ (𝐶 ∈ (LocFin‘𝒫
𝑋) → 𝑋 = 𝑌) | 
| 6 | 1, 5 | jca 511 | . 2
⊢ (𝐶 ∈ (LocFin‘𝒫
𝑋) → (𝐶 ∈ PtFin ∧ 𝑋 = 𝑌)) | 
| 7 |  | simpr 484 | . . . . 5
⊢ ((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) → 𝑋 = 𝑌) | 
| 8 |  | uniexg 7761 | . . . . . . 7
⊢ (𝐶 ∈ PtFin → ∪ 𝐶
∈ V) | 
| 9 | 4, 8 | eqeltrid 2844 | . . . . . 6
⊢ (𝐶 ∈ PtFin → 𝑌 ∈ V) | 
| 10 | 9 | adantr 480 | . . . . 5
⊢ ((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) → 𝑌 ∈ V) | 
| 11 | 7, 10 | eqeltrd 2840 | . . . 4
⊢ ((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) → 𝑋 ∈ V) | 
| 12 |  | distop 23003 | . . . 4
⊢ (𝑋 ∈ V → 𝒫 𝑋 ∈ Top) | 
| 13 | 11, 12 | syl 17 | . . 3
⊢ ((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) → 𝒫 𝑋 ∈ Top) | 
| 14 |  | snelpwi 5447 | . . . . . 6
⊢ (𝑥 ∈ 𝑋 → {𝑥} ∈ 𝒫 𝑋) | 
| 15 | 14 | adantl 481 | . . . . 5
⊢ (((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ 𝒫 𝑋) | 
| 16 |  | snidg 4659 | . . . . . 6
⊢ (𝑥 ∈ 𝑋 → 𝑥 ∈ {𝑥}) | 
| 17 | 16 | adantl 481 | . . . . 5
⊢ (((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ {𝑥}) | 
| 18 |  | simpll 766 | . . . . . 6
⊢ (((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ PtFin) | 
| 19 | 7 | eleq2d 2826 | . . . . . . 7
⊢ ((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ 𝑌)) | 
| 20 | 19 | biimpa 476 | . . . . . 6
⊢ (((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑌) | 
| 21 | 4 | ptfinfin 23528 | . . . . . 6
⊢ ((𝐶 ∈ PtFin ∧ 𝑥 ∈ 𝑌) → {𝑠 ∈ 𝐶 ∣ 𝑥 ∈ 𝑠} ∈ Fin) | 
| 22 | 18, 20, 21 | syl2anc 584 | . . . . 5
⊢ (((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) ∧ 𝑥 ∈ 𝑋) → {𝑠 ∈ 𝐶 ∣ 𝑥 ∈ 𝑠} ∈ Fin) | 
| 23 |  | eleq2 2829 | . . . . . . 7
⊢ (𝑦 = {𝑥} → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ {𝑥})) | 
| 24 |  | ineq2 4213 | . . . . . . . . . . 11
⊢ (𝑦 = {𝑥} → (𝑠 ∩ 𝑦) = (𝑠 ∩ {𝑥})) | 
| 25 | 24 | neeq1d 2999 | . . . . . . . . . 10
⊢ (𝑦 = {𝑥} → ((𝑠 ∩ 𝑦) ≠ ∅ ↔ (𝑠 ∩ {𝑥}) ≠ ∅)) | 
| 26 |  | disjsn 4710 | . . . . . . . . . . 11
⊢ ((𝑠 ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ 𝑠) | 
| 27 | 26 | necon2abii 2990 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝑠 ↔ (𝑠 ∩ {𝑥}) ≠ ∅) | 
| 28 | 25, 27 | bitr4di 289 | . . . . . . . . 9
⊢ (𝑦 = {𝑥} → ((𝑠 ∩ 𝑦) ≠ ∅ ↔ 𝑥 ∈ 𝑠)) | 
| 29 | 28 | rabbidv 3443 | . . . . . . . 8
⊢ (𝑦 = {𝑥} → {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑦) ≠ ∅} = {𝑠 ∈ 𝐶 ∣ 𝑥 ∈ 𝑠}) | 
| 30 | 29 | eleq1d 2825 | . . . . . . 7
⊢ (𝑦 = {𝑥} → ({𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑦) ≠ ∅} ∈ Fin ↔ {𝑠 ∈ 𝐶 ∣ 𝑥 ∈ 𝑠} ∈ Fin)) | 
| 31 | 23, 30 | anbi12d 632 | . . . . . 6
⊢ (𝑦 = {𝑥} → ((𝑥 ∈ 𝑦 ∧ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑦) ≠ ∅} ∈ Fin) ↔ (𝑥 ∈ {𝑥} ∧ {𝑠 ∈ 𝐶 ∣ 𝑥 ∈ 𝑠} ∈ Fin))) | 
| 32 | 31 | rspcev 3621 | . . . . 5
⊢ (({𝑥} ∈ 𝒫 𝑋 ∧ (𝑥 ∈ {𝑥} ∧ {𝑠 ∈ 𝐶 ∣ 𝑥 ∈ 𝑠} ∈ Fin)) → ∃𝑦 ∈ 𝒫 𝑋(𝑥 ∈ 𝑦 ∧ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑦) ≠ ∅} ∈ Fin)) | 
| 33 | 15, 17, 22, 32 | syl12anc 836 | . . . 4
⊢ (((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) ∧ 𝑥 ∈ 𝑋) → ∃𝑦 ∈ 𝒫 𝑋(𝑥 ∈ 𝑦 ∧ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑦) ≠ ∅} ∈ Fin)) | 
| 34 | 33 | ralrimiva 3145 | . . 3
⊢ ((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) → ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝒫 𝑋(𝑥 ∈ 𝑦 ∧ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑦) ≠ ∅} ∈ Fin)) | 
| 35 | 3, 4 | islocfin 23526 | . . 3
⊢ (𝐶 ∈ (LocFin‘𝒫
𝑋) ↔ (𝒫 𝑋 ∈ Top ∧ 𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝒫 𝑋(𝑥 ∈ 𝑦 ∧ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑦) ≠ ∅} ∈
Fin))) | 
| 36 | 13, 7, 34, 35 | syl3anbrc 1343 | . 2
⊢ ((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) → 𝐶 ∈ (LocFin‘𝒫 𝑋)) | 
| 37 | 6, 36 | impbii 209 | 1
⊢ (𝐶 ∈ (LocFin‘𝒫
𝑋) ↔ (𝐶 ∈ PtFin ∧ 𝑋 = 𝑌)) |