Metamath Proof Explorer


Theorem dissnlocfin

Description: The set of singletons is locally finite in the discrete topology. (Contributed by Thierry Arnoux, 9-Jan-2020)

Ref Expression
Hypothesis dissnref.c C=u|xXu=x
Assertion dissnlocfin XVCLocFin𝒫X

Proof

Step Hyp Ref Expression
1 dissnref.c C=u|xXu=x
2 distop XV𝒫XTop
3 eqidd XVX=X
4 snelpwi zXz𝒫X
5 4 adantl XVzXz𝒫X
6 vsnid zz
7 6 a1i XVzXzz
8 nfv uXVzX
9 nfrab1 _uuC|uz
10 nfcv _uz
11 1 abeq2i uCxXu=x
12 11 anbi1i uCuzxXu=xuz
13 simpr XVzXuzxXu=xu=x
14 simplr XVzXuzxXu=xxzu=x
15 14 ineq1d XVzXuzxXu=xxzuz=xz
16 disjsn2 xzxz=
17 16 adantl XVzXuzxXu=xxzxz=
18 15 17 eqtrd XVzXuzxXu=xxzuz=
19 simp-4r XVzXuzxXu=xxzuz
20 19 neneqd XVzXuzxXu=xxz¬uz=
21 18 20 pm2.65da XVzXuzxXu=x¬xz
22 nne ¬xzx=z
23 21 22 sylib XVzXuzxXu=xx=z
24 23 sneqd XVzXuzxXu=xx=z
25 13 24 eqtrd XVzXuzxXu=xu=z
26 25 r19.29an XVzXuzxXu=xu=z
27 26 an32s XVzXxXu=xuzu=z
28 27 anasss XVzXxXu=xuzu=z
29 sneq x=zx=z
30 29 rspceeqv zXu=zxXu=x
31 30 adantll XVzXu=zxXu=x
32 simpr XVzXu=zu=z
33 32 ineq1d XVzXu=zuz=zz
34 inidm zz=z
35 33 34 eqtrdi XVzXu=zuz=z
36 vex zV
37 36 snnz z
38 37 a1i XVzXu=zz
39 35 38 eqnetrd XVzXu=zuz
40 31 39 jca XVzXu=zxXu=xuz
41 28 40 impbida XVzXxXu=xuzu=z
42 12 41 syl5bb XVzXuCuzu=z
43 rabid uuC|uzuCuz
44 velsn uzu=z
45 42 43 44 3bitr4g XVzXuuC|uzuz
46 8 9 10 45 eqrd XVzXuC|uz=z
47 snfi zFin
48 46 47 eqeltrdi XVzXuC|uzFin
49 eleq2 y=zzyzz
50 ineq2 y=zuy=uz
51 50 neeq1d y=zuyuz
52 51 rabbidv y=zuC|uy=uC|uz
53 52 eleq1d y=zuC|uyFinuC|uzFin
54 49 53 anbi12d y=zzyuC|uyFinzzuC|uzFin
55 54 rspcev z𝒫XzzuC|uzFiny𝒫XzyuC|uyFin
56 5 7 48 55 syl12anc XVzXy𝒫XzyuC|uyFin
57 56 ralrimiva XVzXy𝒫XzyuC|uyFin
58 unipw 𝒫X=X
59 58 eqcomi X=𝒫X
60 1 unisngl X=C
61 59 60 islocfin CLocFin𝒫X𝒫XTopX=XzXy𝒫XzyuC|uyFin
62 2 3 57 61 syl3anbrc XVCLocFin𝒫X