Metamath Proof Explorer


Theorem locfindis

Description: The locally finite covers of a discrete space are precisely the point-finite covers. (Contributed by Jeff Hankins, 22-Jan-2010) (Proof shortened by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypothesis locfindis.1 Y=C
Assertion locfindis CLocFin𝒫XCPtFinX=Y

Proof

Step Hyp Ref Expression
1 locfindis.1 Y=C
2 lfinpfin CLocFin𝒫XCPtFin
3 unipw 𝒫X=X
4 3 eqcomi X=𝒫X
5 4 1 locfinbas CLocFin𝒫XX=Y
6 2 5 jca CLocFin𝒫XCPtFinX=Y
7 simpr CPtFinX=YX=Y
8 uniexg CPtFinCV
9 1 8 eqeltrid CPtFinYV
10 9 adantr CPtFinX=YYV
11 7 10 eqeltrd CPtFinX=YXV
12 distop XV𝒫XTop
13 11 12 syl CPtFinX=Y𝒫XTop
14 snelpwi xXx𝒫X
15 14 adantl CPtFinX=YxXx𝒫X
16 snidg xXxx
17 16 adantl CPtFinX=YxXxx
18 simpll CPtFinX=YxXCPtFin
19 7 eleq2d CPtFinX=YxXxY
20 19 biimpa CPtFinX=YxXxY
21 1 ptfinfin CPtFinxYsC|xsFin
22 18 20 21 syl2anc CPtFinX=YxXsC|xsFin
23 eleq2 y=xxyxx
24 ineq2 y=xsy=sx
25 24 neeq1d y=xsysx
26 disjsn sx=¬xs
27 26 necon2abii xssx
28 25 27 bitr4di y=xsyxs
29 28 rabbidv y=xsC|sy=sC|xs
30 29 eleq1d y=xsC|syFinsC|xsFin
31 23 30 anbi12d y=xxysC|syFinxxsC|xsFin
32 31 rspcev x𝒫XxxsC|xsFiny𝒫XxysC|syFin
33 15 17 22 32 syl12anc CPtFinX=YxXy𝒫XxysC|syFin
34 33 ralrimiva CPtFinX=YxXy𝒫XxysC|syFin
35 4 1 islocfin CLocFin𝒫X𝒫XTopX=YxXy𝒫XxysC|syFin
36 13 7 34 35 syl3anbrc CPtFinX=YCLocFin𝒫X
37 6 36 impbii CLocFin𝒫XCPtFinX=Y