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 | |
|
Assertion | dscopn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dscmet.1 | |
|
2 | 1 | dscmet | |
3 | metxmet | |
|
4 | 2 3 | syl | |
5 | eqid | |
|
6 | 5 | elmopn | |
7 | 4 6 | syl | |
8 | simpll | |
|
9 | ssel2 | |
|
10 | 9 | adantll | |
11 | 8 10 | jca | |
12 | velsn | |
|
13 | eleq1a | |
|
14 | simpl | |
|
15 | 14 | a1i | |
16 | eqeq12 | |
|
17 | 16 | ifbid | |
18 | 0re | |
|
19 | 1re | |
|
20 | 18 19 | ifcli | |
21 | 20 | elexi | |
22 | 17 1 21 | ovmpoa | |
23 | 22 | breq1d | |
24 | 19 | ltnri | |
25 | iffalse | |
|
26 | 25 | breq1d | |
27 | 24 26 | mtbiri | |
28 | 27 | con4i | |
29 | iftrue | |
|
30 | 0lt1 | |
|
31 | 29 30 | eqbrtrdi | |
32 | 28 31 | impbii | |
33 | equcom | |
|
34 | 32 33 | bitri | |
35 | 23 34 | bitr2di | |
36 | simpr | |
|
37 | 36 | biantrurd | |
38 | 35 37 | bitrd | |
39 | 38 | ex | |
40 | 13 15 39 | pm5.21ndd | |
41 | 40 | adantl | |
42 | 1xr | |
|
43 | elbl | |
|
44 | 42 43 | mp3an3 | |
45 | 4 44 | sylan | |
46 | 41 45 | bitr4d | |
47 | 12 46 | syl5bb | |
48 | 47 | eqrdv | |
49 | blelrn | |
|
50 | 42 49 | mp3an3 | |
51 | 4 50 | sylan | |
52 | 48 51 | eqeltrd | |
53 | snssi | |
|
54 | vsnid | |
|
55 | 53 54 | jctil | |
56 | eleq2 | |
|
57 | sseq1 | |
|
58 | 56 57 | anbi12d | |
59 | 58 | rspcev | |
60 | 52 55 59 | syl2an | |
61 | 11 60 | sylancom | |
62 | 61 | ralrimiva | |
63 | 62 | ex | |
64 | 63 | pm4.71d | |
65 | 7 64 | bitr4d | |
66 | velpw | |
|
67 | 65 66 | bitr4di | |
68 | 67 | eqrdv | |