Metamath Proof Explorer


Theorem dscopn

Description: The discrete metric generates the discrete topology. In particular, the discrete topology is metrizable. (Contributed by Mario Carneiro, 29-Jan-2014)

Ref Expression
Hypothesis dscmet.1 D=xX,yXifx=y01
Assertion dscopn XVMetOpenD=𝒫X

Proof

Step Hyp Ref Expression
1 dscmet.1 D=xX,yXifx=y01
2 1 dscmet XVDMetX
3 metxmet DMetXD∞MetX
4 2 3 syl XVD∞MetX
5 eqid MetOpenD=MetOpenD
6 5 elmopn D∞MetXuMetOpenDuXvuwranballDvwwu
7 4 6 syl XVuMetOpenDuXvuwranballDvwwu
8 simpll XVuXvuXV
9 ssel2 uXvuvX
10 9 adantll XVuXvuvX
11 8 10 jca XVuXvuXVvX
12 velsn wvw=v
13 eleq1a vXw=vwX
14 simpl wXvDw<1wX
15 14 a1i vXwXvDw<1wX
16 eqeq12 x=vy=wx=yv=w
17 16 ifbid x=vy=wifx=y01=ifv=w01
18 0re 0
19 1re 1
20 18 19 ifcli ifv=w01
21 20 elexi ifv=w01V
22 17 1 21 ovmpoa vXwXvDw=ifv=w01
23 22 breq1d vXwXvDw<1ifv=w01<1
24 19 ltnri ¬1<1
25 iffalse ¬v=wifv=w01=1
26 25 breq1d ¬v=wifv=w01<11<1
27 24 26 mtbiri ¬v=w¬ifv=w01<1
28 27 con4i ifv=w01<1v=w
29 iftrue v=wifv=w01=0
30 0lt1 0<1
31 29 30 eqbrtrdi v=wifv=w01<1
32 28 31 impbii ifv=w01<1v=w
33 equcom v=ww=v
34 32 33 bitri ifv=w01<1w=v
35 23 34 bitr2di vXwXw=vvDw<1
36 simpr vXwXwX
37 36 biantrurd vXwXvDw<1wXvDw<1
38 35 37 bitrd vXwXw=vwXvDw<1
39 38 ex vXwXw=vwXvDw<1
40 13 15 39 pm5.21ndd vXw=vwXvDw<1
41 40 adantl XVvXw=vwXvDw<1
42 1xr 1*
43 elbl D∞MetXvX1*wvballD1wXvDw<1
44 42 43 mp3an3 D∞MetXvXwvballD1wXvDw<1
45 4 44 sylan XVvXwvballD1wXvDw<1
46 41 45 bitr4d XVvXw=vwvballD1
47 12 46 syl5bb XVvXwvwvballD1
48 47 eqrdv XVvXv=vballD1
49 blelrn D∞MetXvX1*vballD1ranballD
50 42 49 mp3an3 D∞MetXvXvballD1ranballD
51 4 50 sylan XVvXvballD1ranballD
52 48 51 eqeltrd XVvXvranballD
53 snssi vuvu
54 vsnid vv
55 53 54 jctil vuvvvu
56 eleq2 w=vvwvv
57 sseq1 w=vwuvu
58 56 57 anbi12d w=vvwwuvvvu
59 58 rspcev vranballDvvvuwranballDvwwu
60 52 55 59 syl2an XVvXvuwranballDvwwu
61 11 60 sylancom XVuXvuwranballDvwwu
62 61 ralrimiva XVuXvuwranballDvwwu
63 62 ex XVuXvuwranballDvwwu
64 63 pm4.71d XVuXuXvuwranballDvwwu
65 7 64 bitr4d XVuMetOpenDuX
66 velpw u𝒫XuX
67 65 66 bitr4di XVuMetOpenDu𝒫X
68 67 eqrdv XVMetOpenD=𝒫X