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 = x ∈ X , y ∈ X ⟼ if x = y 0 1
Assertion dscopn ⊢ X ∈ V → MetOpen ⁡ D = 𝒫 X

Proof

Step Hyp Ref Expression
1 dscmet.1 ⊢ D = x ∈ X , y ∈ X ⟼ if x = y 0 1
2 1 dscmet ⊢ X ∈ V → D ∈ Met ⁡ X
3 metxmet ⊢ D ∈ Met ⁡ X → D ∈ ∞Met ⁡ X
4 2 3 syl ⊢ X ∈ V → D ∈ ∞Met ⁡ X
5 eqid ⊢ MetOpen ⁡ D = MetOpen ⁡ D
6 5 elmopn ⊢ D ∈ ∞Met ⁡ X → u ∈ MetOpen ⁡ D ↔ u ⊆ X ∧ ∀ v ∈ u ∃ w ∈ ran ⁡ ball ⁡ D v ∈ w ∧ w ⊆ u
7 4 6 syl ⊢ X ∈ V → u ∈ MetOpen ⁡ D ↔ u ⊆ X ∧ ∀ v ∈ u ∃ w ∈ ran ⁡ ball ⁡ D v ∈ w ∧ w ⊆ u
8 simpll ⊢ X ∈ V ∧ u ⊆ X ∧ v ∈ u → X ∈ V
9 ssel2 ⊢ u ⊆ X ∧ v ∈ u → v ∈ X
10 9 adantll ⊢ X ∈ V ∧ u ⊆ X ∧ v ∈ u → v ∈ X
11 8 10 jca ⊢ X ∈ V ∧ u ⊆ X ∧ v ∈ u → X ∈ V ∧ v ∈ X
12 velsn ⊢ w ∈ v ↔ w = v
13 eleq1a ⊢ v ∈ X → w = v → w ∈ X
14 simpl ⊢ w ∈ X ∧ v D w < 1 → w ∈ X
15 14 a1i ⊢ v ∈ X → w ∈ X ∧ v D w < 1 → w ∈ X
16 eqeq12 ⊢ x = v ∧ y = w → x = y ↔ v = w
17 16 ifbid ⊢ x = v ∧ y = w → if x = y 0 1 = if v = w 0 1
18 0re ⊢ 0 ∈ ℝ
19 1re ⊢ 1 ∈ ℝ
20 18 19 ifcli ⊢ if v = w 0 1 ∈ ℝ
21 20 elexi ⊢ if v = w 0 1 ∈ V
22 17 1 21 ovmpoa ⊢ v ∈ X ∧ w ∈ X → v D w = if v = w 0 1
23 22 breq1d ⊢ v ∈ X ∧ w ∈ X → v D w < 1 ↔ if v = w 0 1 < 1
24 19 ltnri ⊢ ¬ 1 < 1
25 iffalse ⊢ ¬ v = w → if v = w 0 1 = 1
26 25 breq1d ⊢ ¬ v = w → if v = w 0 1 < 1 ↔ 1 < 1
27 24 26 mtbiri ⊢ ¬ v = w → ¬ if v = w 0 1 < 1
28 27 con4i ⊢ if v = w 0 1 < 1 → v = w
29 iftrue ⊢ v = w → if v = w 0 1 = 0
30 0lt1 ⊢ 0 < 1
31 29 30 eqbrtrdi ⊢ v = w → if v = w 0 1 < 1
32 28 31 impbii ⊢ if v = w 0 1 < 1 ↔ v = w
33 equcom ⊢ v = w ↔ w = v
34 32 33 bitri ⊢ if v = w 0 1 < 1 ↔ w = v
35 23 34 bitr2di ⊢ v ∈ X ∧ w ∈ X → w = v ↔ v D w < 1
36 simpr ⊢ v ∈ X ∧ w ∈ X → w ∈ X
37 36 biantrurd ⊢ v ∈ X ∧ w ∈ X → v D w < 1 ↔ w ∈ X ∧ v D w < 1
38 35 37 bitrd ⊢ v ∈ X ∧ w ∈ X → w = v ↔ w ∈ X ∧ v D w < 1
39 38 ex ⊢ v ∈ X → w ∈ X → w = v ↔ w ∈ X ∧ v D w < 1
40 13 15 39 pm5.21ndd ⊢ v ∈ X → w = v ↔ w ∈ X ∧ v D w < 1
41 40 adantl ⊢ X ∈ V ∧ v ∈ X → w = v ↔ w ∈ X ∧ v D w < 1
42 1xr ⊢ 1 ∈ ℝ *
43 elbl ⊢ D ∈ ∞Met ⁡ X ∧ v ∈ X ∧ 1 ∈ ℝ * → w ∈ v ball ⁡ D 1 ↔ w ∈ X ∧ v D w < 1
44 42 43 mp3an3 ⊢ D ∈ ∞Met ⁡ X ∧ v ∈ X → w ∈ v ball ⁡ D 1 ↔ w ∈ X ∧ v D w < 1
45 4 44 sylan ⊢ X ∈ V ∧ v ∈ X → w ∈ v ball ⁡ D 1 ↔ w ∈ X ∧ v D w < 1
46 41 45 bitr4d ⊢ X ∈ V ∧ v ∈ X → w = v ↔ w ∈ v ball ⁡ D 1
47 12 46 syl5bb ⊢ X ∈ V ∧ v ∈ X → w ∈ v ↔ w ∈ v ball ⁡ D 1
48 47 eqrdv ⊢ X ∈ V ∧ v ∈ X → v = v ball ⁡ D 1
49 blelrn ⊢ D ∈ ∞Met ⁡ X ∧ v ∈ X ∧ 1 ∈ ℝ * → v ball ⁡ D 1 ∈ ran ⁡ ball ⁡ D
50 42 49 mp3an3 ⊢ D ∈ ∞Met ⁡ X ∧ v ∈ X → v ball ⁡ D 1 ∈ ran ⁡ ball ⁡ D
51 4 50 sylan ⊢ X ∈ V ∧ v ∈ X → v ball ⁡ D 1 ∈ ran ⁡ ball ⁡ D
52 48 51 eqeltrd ⊢ X ∈ V ∧ v ∈ X → v ∈ ran ⁡ ball ⁡ D
53 snssi ⊢ v ∈ u → v ⊆ u
54 vsnid ⊢ v ∈ v
55 53 54 jctil ⊢ v ∈ u → v ∈ v ∧ v ⊆ u
56 eleq2 ⊢ w = v → v ∈ w ↔ v ∈ v
57 sseq1 ⊢ w = v → w ⊆ u ↔ v ⊆ u
58 56 57 anbi12d ⊢ w = v → v ∈ w ∧ w ⊆ u ↔ v ∈ v ∧ v ⊆ u
59 58 rspcev ⊢ v ∈ ran ⁡ ball ⁡ D ∧ v ∈ v ∧ v ⊆ u → ∃ w ∈ ran ⁡ ball ⁡ D v ∈ w ∧ w ⊆ u
60 52 55 59 syl2an ⊢ X ∈ V ∧ v ∈ X ∧ v ∈ u → ∃ w ∈ ran ⁡ ball ⁡ D v ∈ w ∧ w ⊆ u
61 11 60 sylancom ⊢ X ∈ V ∧ u ⊆ X ∧ v ∈ u → ∃ w ∈ ran ⁡ ball ⁡ D v ∈ w ∧ w ⊆ u
62 61 ralrimiva ⊢ X ∈ V ∧ u ⊆ X → ∀ v ∈ u ∃ w ∈ ran ⁡ ball ⁡ D v ∈ w ∧ w ⊆ u
63 62 ex ⊢ X ∈ V → u ⊆ X → ∀ v ∈ u ∃ w ∈ ran ⁡ ball ⁡ D v ∈ w ∧ w ⊆ u
64 63 pm4.71d ⊢ X ∈ V → u ⊆ X ↔ u ⊆ X ∧ ∀ v ∈ u ∃ w ∈ ran ⁡ ball ⁡ D v ∈ w ∧ w ⊆ u
65 7 64 bitr4d ⊢ X ∈ V → u ∈ MetOpen ⁡ D ↔ u ⊆ X
66 velpw ⊢ u ∈ 𝒫 X ↔ u ⊆ X
67 65 66 bitr4di ⊢ X ∈ V → u ∈ MetOpen ⁡ D ↔ u ∈ 𝒫 X
68 67 eqrdv ⊢ X ∈ V → MetOpen ⁡ D = 𝒫 X