Step | Hyp | Ref
| Expression |
1 | | lfinpfin 21137 |
. . 3
⊢ (𝐶 ∈ (LocFin‘𝒫
𝑋) → 𝐶 ∈ PtFin) |
2 | | unipw 4845 |
. . . . 5
⊢ ∪ 𝒫 𝑋 = 𝑋 |
3 | 2 | eqcomi 2619 |
. . . 4
⊢ 𝑋 = ∪
𝒫 𝑋 |
4 | | locfindis.1 |
. . . 4
⊢ 𝑌 = ∪
𝐶 |
5 | 3, 4 | locfinbas 21135 |
. . 3
⊢ (𝐶 ∈ (LocFin‘𝒫
𝑋) → 𝑋 = 𝑌) |
6 | 1, 5 | jca 553 |
. 2
⊢ (𝐶 ∈ (LocFin‘𝒫
𝑋) → (𝐶 ∈ PtFin ∧ 𝑋 = 𝑌)) |
7 | | simpr 476 |
. . . . 5
⊢ ((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) → 𝑋 = 𝑌) |
8 | | uniexg 6853 |
. . . . . . 7
⊢ (𝐶 ∈ PtFin → ∪ 𝐶
∈ V) |
9 | 4, 8 | syl5eqel 2692 |
. . . . . 6
⊢ (𝐶 ∈ PtFin → 𝑌 ∈ V) |
10 | 9 | adantr 480 |
. . . . 5
⊢ ((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) → 𝑌 ∈ V) |
11 | 7, 10 | eqeltrd 2688 |
. . . 4
⊢ ((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) → 𝑋 ∈ V) |
12 | | distop 20610 |
. . . 4
⊢ (𝑋 ∈ V → 𝒫 𝑋 ∈ Top) |
13 | 11, 12 | syl 17 |
. . 3
⊢ ((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) → 𝒫 𝑋 ∈ Top) |
14 | | snelpwi 4839 |
. . . . . 6
⊢ (𝑥 ∈ 𝑋 → {𝑥} ∈ 𝒫 𝑋) |
15 | 14 | adantl 481 |
. . . . 5
⊢ (((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ 𝒫 𝑋) |
16 | | snidg 4153 |
. . . . . 6
⊢ (𝑥 ∈ 𝑋 → 𝑥 ∈ {𝑥}) |
17 | 16 | adantl 481 |
. . . . 5
⊢ (((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ {𝑥}) |
18 | | simpll 786 |
. . . . . 6
⊢ (((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ PtFin) |
19 | 7 | eleq2d 2673 |
. . . . . . 7
⊢ ((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) → (𝑥 ∈ 𝑋 ↔ 𝑥 ∈ 𝑌)) |
20 | 19 | biimpa 500 |
. . . . . 6
⊢ (((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑌) |
21 | 4 | ptfinfin 21132 |
. . . . . 6
⊢ ((𝐶 ∈ PtFin ∧ 𝑥 ∈ 𝑌) → {𝑠 ∈ 𝐶 ∣ 𝑥 ∈ 𝑠} ∈ Fin) |
22 | 18, 20, 21 | syl2anc 691 |
. . . . 5
⊢ (((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) ∧ 𝑥 ∈ 𝑋) → {𝑠 ∈ 𝐶 ∣ 𝑥 ∈ 𝑠} ∈ Fin) |
23 | | eleq2 2677 |
. . . . . . 7
⊢ (𝑦 = {𝑥} → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ {𝑥})) |
24 | | ineq2 3770 |
. . . . . . . . . . 11
⊢ (𝑦 = {𝑥} → (𝑠 ∩ 𝑦) = (𝑠 ∩ {𝑥})) |
25 | 24 | neeq1d 2841 |
. . . . . . . . . 10
⊢ (𝑦 = {𝑥} → ((𝑠 ∩ 𝑦) ≠ ∅ ↔ (𝑠 ∩ {𝑥}) ≠ ∅)) |
26 | | disjsn 4192 |
. . . . . . . . . . 11
⊢ ((𝑠 ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ 𝑠) |
27 | 26 | necon2abii 2832 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑠 ↔ (𝑠 ∩ {𝑥}) ≠ ∅) |
28 | 25, 27 | syl6bbr 277 |
. . . . . . . . 9
⊢ (𝑦 = {𝑥} → ((𝑠 ∩ 𝑦) ≠ ∅ ↔ 𝑥 ∈ 𝑠)) |
29 | 28 | rabbidv 3164 |
. . . . . . . 8
⊢ (𝑦 = {𝑥} → {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑦) ≠ ∅} = {𝑠 ∈ 𝐶 ∣ 𝑥 ∈ 𝑠}) |
30 | 29 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑦 = {𝑥} → ({𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑦) ≠ ∅} ∈ Fin ↔ {𝑠 ∈ 𝐶 ∣ 𝑥 ∈ 𝑠} ∈ Fin)) |
31 | 23, 30 | anbi12d 743 |
. . . . . 6
⊢ (𝑦 = {𝑥} → ((𝑥 ∈ 𝑦 ∧ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑦) ≠ ∅} ∈ Fin) ↔ (𝑥 ∈ {𝑥} ∧ {𝑠 ∈ 𝐶 ∣ 𝑥 ∈ 𝑠} ∈ Fin))) |
32 | 31 | rspcev 3282 |
. . . . 5
⊢ (({𝑥} ∈ 𝒫 𝑋 ∧ (𝑥 ∈ {𝑥} ∧ {𝑠 ∈ 𝐶 ∣ 𝑥 ∈ 𝑠} ∈ Fin)) → ∃𝑦 ∈ 𝒫 𝑋(𝑥 ∈ 𝑦 ∧ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑦) ≠ ∅} ∈ Fin)) |
33 | 15, 17, 22, 32 | syl12anc 1316 |
. . . 4
⊢ (((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) ∧ 𝑥 ∈ 𝑋) → ∃𝑦 ∈ 𝒫 𝑋(𝑥 ∈ 𝑦 ∧ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑦) ≠ ∅} ∈ Fin)) |
34 | 33 | ralrimiva 2949 |
. . 3
⊢ ((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) → ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝒫 𝑋(𝑥 ∈ 𝑦 ∧ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑦) ≠ ∅} ∈ Fin)) |
35 | 3, 4 | islocfin 21130 |
. . 3
⊢ (𝐶 ∈ (LocFin‘𝒫
𝑋) ↔ (𝒫 𝑋 ∈ Top ∧ 𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝒫 𝑋(𝑥 ∈ 𝑦 ∧ {𝑠 ∈ 𝐶 ∣ (𝑠 ∩ 𝑦) ≠ ∅} ∈
Fin))) |
36 | 13, 7, 34, 35 | syl3anbrc 1239 |
. 2
⊢ ((𝐶 ∈ PtFin ∧ 𝑋 = 𝑌) → 𝐶 ∈ (LocFin‘𝒫 𝑋)) |
37 | 6, 36 | impbii 198 |
1
⊢ (𝐶 ∈ (LocFin‘𝒫
𝑋) ↔ (𝐶 ∈ PtFin ∧ 𝑋 = 𝑌)) |