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 ⊒ 𝐷 = ( π‘₯ ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ if ( π‘₯ = 𝑦 , 0 , 1 ) )
Assertion dscopn ( 𝑋 ∈ 𝑉 β†’ ( MetOpen β€˜ 𝐷 ) = 𝒫 𝑋 )

Proof

Step Hyp Ref Expression
1 dscmet.1 ⊒ 𝐷 = ( π‘₯ ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ if ( π‘₯ = 𝑦 , 0 , 1 ) )
2 1 dscmet ⊒ ( 𝑋 ∈ 𝑉 β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
3 metxmet ⊒ ( 𝐷 ∈ ( Met β€˜ 𝑋 ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
4 2 3 syl ⊒ ( 𝑋 ∈ 𝑉 β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
5 eqid ⊒ ( MetOpen β€˜ 𝐷 ) = ( MetOpen β€˜ 𝐷 )
6 5 elmopn ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ( 𝑒 ∈ ( MetOpen β€˜ 𝐷 ) ↔ ( 𝑒 βŠ† 𝑋 ∧ βˆ€ 𝑣 ∈ 𝑒 βˆƒ 𝑀 ∈ ran ( ball β€˜ 𝐷 ) ( 𝑣 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑒 ) ) ) )
7 4 6 syl ⊒ ( 𝑋 ∈ 𝑉 β†’ ( 𝑒 ∈ ( MetOpen β€˜ 𝐷 ) ↔ ( 𝑒 βŠ† 𝑋 ∧ βˆ€ 𝑣 ∈ 𝑒 βˆƒ 𝑀 ∈ ran ( ball β€˜ 𝐷 ) ( 𝑣 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑒 ) ) ) )
8 simpll ⊒ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑒 βŠ† 𝑋 ) ∧ 𝑣 ∈ 𝑒 ) β†’ 𝑋 ∈ 𝑉 )
9 ssel2 ⊒ ( ( 𝑒 βŠ† 𝑋 ∧ 𝑣 ∈ 𝑒 ) β†’ 𝑣 ∈ 𝑋 )
10 9 adantll ⊒ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑒 βŠ† 𝑋 ) ∧ 𝑣 ∈ 𝑒 ) β†’ 𝑣 ∈ 𝑋 )
11 8 10 jca ⊒ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑒 βŠ† 𝑋 ) ∧ 𝑣 ∈ 𝑒 ) β†’ ( 𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋 ) )
12 velsn ⊒ ( 𝑀 ∈ { 𝑣 } ↔ 𝑀 = 𝑣 )
13 eleq1a ⊒ ( 𝑣 ∈ 𝑋 β†’ ( 𝑀 = 𝑣 β†’ 𝑀 ∈ 𝑋 ) )
14 simpl ⊒ ( ( 𝑀 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑀 ) < 1 ) β†’ 𝑀 ∈ 𝑋 )
15 14 a1i ⊒ ( 𝑣 ∈ 𝑋 β†’ ( ( 𝑀 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑀 ) < 1 ) β†’ 𝑀 ∈ 𝑋 ) )
16 eqeq12 ⊒ ( ( π‘₯ = 𝑣 ∧ 𝑦 = 𝑀 ) β†’ ( π‘₯ = 𝑦 ↔ 𝑣 = 𝑀 ) )
17 16 ifbid ⊒ ( ( π‘₯ = 𝑣 ∧ 𝑦 = 𝑀 ) β†’ if ( π‘₯ = 𝑦 , 0 , 1 ) = if ( 𝑣 = 𝑀 , 0 , 1 ) )
18 0re ⊒ 0 ∈ ℝ
19 1re ⊒ 1 ∈ ℝ
20 18 19 ifcli ⊒ if ( 𝑣 = 𝑀 , 0 , 1 ) ∈ ℝ
21 20 elexi ⊒ if ( 𝑣 = 𝑀 , 0 , 1 ) ∈ V
22 17 1 21 ovmpoa ⊒ ( ( 𝑣 ∈ 𝑋 ∧ 𝑀 ∈ 𝑋 ) β†’ ( 𝑣 𝐷 𝑀 ) = if ( 𝑣 = 𝑀 , 0 , 1 ) )
23 22 breq1d ⊒ ( ( 𝑣 ∈ 𝑋 ∧ 𝑀 ∈ 𝑋 ) β†’ ( ( 𝑣 𝐷 𝑀 ) < 1 ↔ if ( 𝑣 = 𝑀 , 0 , 1 ) < 1 ) )
24 19 ltnri ⊒ ¬ 1 < 1
25 iffalse ⊒ ( Β¬ 𝑣 = 𝑀 β†’ if ( 𝑣 = 𝑀 , 0 , 1 ) = 1 )
26 25 breq1d ⊒ ( Β¬ 𝑣 = 𝑀 β†’ ( if ( 𝑣 = 𝑀 , 0 , 1 ) < 1 ↔ 1 < 1 ) )
27 24 26 mtbiri ⊒ ( Β¬ 𝑣 = 𝑀 β†’ Β¬ if ( 𝑣 = 𝑀 , 0 , 1 ) < 1 )
28 27 con4i ⊒ ( if ( 𝑣 = 𝑀 , 0 , 1 ) < 1 β†’ 𝑣 = 𝑀 )
29 iftrue ⊒ ( 𝑣 = 𝑀 β†’ if ( 𝑣 = 𝑀 , 0 , 1 ) = 0 )
30 0lt1 ⊒ 0 < 1
31 29 30 eqbrtrdi ⊒ ( 𝑣 = 𝑀 β†’ if ( 𝑣 = 𝑀 , 0 , 1 ) < 1 )
32 28 31 impbii ⊒ ( if ( 𝑣 = 𝑀 , 0 , 1 ) < 1 ↔ 𝑣 = 𝑀 )
33 equcom ⊒ ( 𝑣 = 𝑀 ↔ 𝑀 = 𝑣 )
34 32 33 bitri ⊒ ( if ( 𝑣 = 𝑀 , 0 , 1 ) < 1 ↔ 𝑀 = 𝑣 )
35 23 34 bitr2di ⊒ ( ( 𝑣 ∈ 𝑋 ∧ 𝑀 ∈ 𝑋 ) β†’ ( 𝑀 = 𝑣 ↔ ( 𝑣 𝐷 𝑀 ) < 1 ) )
36 simpr ⊒ ( ( 𝑣 ∈ 𝑋 ∧ 𝑀 ∈ 𝑋 ) β†’ 𝑀 ∈ 𝑋 )
37 36 biantrurd ⊒ ( ( 𝑣 ∈ 𝑋 ∧ 𝑀 ∈ 𝑋 ) β†’ ( ( 𝑣 𝐷 𝑀 ) < 1 ↔ ( 𝑀 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑀 ) < 1 ) ) )
38 35 37 bitrd ⊒ ( ( 𝑣 ∈ 𝑋 ∧ 𝑀 ∈ 𝑋 ) β†’ ( 𝑀 = 𝑣 ↔ ( 𝑀 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑀 ) < 1 ) ) )
39 38 ex ⊒ ( 𝑣 ∈ 𝑋 β†’ ( 𝑀 ∈ 𝑋 β†’ ( 𝑀 = 𝑣 ↔ ( 𝑀 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑀 ) < 1 ) ) ) )
40 13 15 39 pm5.21ndd ⊒ ( 𝑣 ∈ 𝑋 β†’ ( 𝑀 = 𝑣 ↔ ( 𝑀 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑀 ) < 1 ) ) )
41 40 adantl ⊒ ( ( 𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋 ) β†’ ( 𝑀 = 𝑣 ↔ ( 𝑀 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑀 ) < 1 ) ) )
42 1xr ⊒ 1 ∈ ℝ*
43 elbl ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑣 ∈ 𝑋 ∧ 1 ∈ ℝ* ) β†’ ( 𝑀 ∈ ( 𝑣 ( ball β€˜ 𝐷 ) 1 ) ↔ ( 𝑀 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑀 ) < 1 ) ) )
44 42 43 mp3an3 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑣 ∈ 𝑋 ) β†’ ( 𝑀 ∈ ( 𝑣 ( ball β€˜ 𝐷 ) 1 ) ↔ ( 𝑀 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑀 ) < 1 ) ) )
45 4 44 sylan ⊒ ( ( 𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋 ) β†’ ( 𝑀 ∈ ( 𝑣 ( ball β€˜ 𝐷 ) 1 ) ↔ ( 𝑀 ∈ 𝑋 ∧ ( 𝑣 𝐷 𝑀 ) < 1 ) ) )
46 41 45 bitr4d ⊒ ( ( 𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋 ) β†’ ( 𝑀 = 𝑣 ↔ 𝑀 ∈ ( 𝑣 ( ball β€˜ 𝐷 ) 1 ) ) )
47 12 46 bitrid ⊒ ( ( 𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋 ) β†’ ( 𝑀 ∈ { 𝑣 } ↔ 𝑀 ∈ ( 𝑣 ( ball β€˜ 𝐷 ) 1 ) ) )
48 47 eqrdv ⊒ ( ( 𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋 ) β†’ { 𝑣 } = ( 𝑣 ( ball β€˜ 𝐷 ) 1 ) )
49 blelrn ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑣 ∈ 𝑋 ∧ 1 ∈ ℝ* ) β†’ ( 𝑣 ( ball β€˜ 𝐷 ) 1 ) ∈ ran ( ball β€˜ 𝐷 ) )
50 42 49 mp3an3 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑣 ∈ 𝑋 ) β†’ ( 𝑣 ( ball β€˜ 𝐷 ) 1 ) ∈ ran ( ball β€˜ 𝐷 ) )
51 4 50 sylan ⊒ ( ( 𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋 ) β†’ ( 𝑣 ( ball β€˜ 𝐷 ) 1 ) ∈ ran ( ball β€˜ 𝐷 ) )
52 48 51 eqeltrd ⊒ ( ( 𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋 ) β†’ { 𝑣 } ∈ ran ( ball β€˜ 𝐷 ) )
53 snssi ⊒ ( 𝑣 ∈ 𝑒 β†’ { 𝑣 } βŠ† 𝑒 )
54 vsnid ⊒ 𝑣 ∈ { 𝑣 }
55 53 54 jctil ⊒ ( 𝑣 ∈ 𝑒 β†’ ( 𝑣 ∈ { 𝑣 } ∧ { 𝑣 } βŠ† 𝑒 ) )
56 eleq2 ⊒ ( 𝑀 = { 𝑣 } β†’ ( 𝑣 ∈ 𝑀 ↔ 𝑣 ∈ { 𝑣 } ) )
57 sseq1 ⊒ ( 𝑀 = { 𝑣 } β†’ ( 𝑀 βŠ† 𝑒 ↔ { 𝑣 } βŠ† 𝑒 ) )
58 56 57 anbi12d ⊒ ( 𝑀 = { 𝑣 } β†’ ( ( 𝑣 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑒 ) ↔ ( 𝑣 ∈ { 𝑣 } ∧ { 𝑣 } βŠ† 𝑒 ) ) )
59 58 rspcev ⊒ ( ( { 𝑣 } ∈ ran ( ball β€˜ 𝐷 ) ∧ ( 𝑣 ∈ { 𝑣 } ∧ { 𝑣 } βŠ† 𝑒 ) ) β†’ βˆƒ 𝑀 ∈ ran ( ball β€˜ 𝐷 ) ( 𝑣 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑒 ) )
60 52 55 59 syl2an ⊒ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑣 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑒 ) β†’ βˆƒ 𝑀 ∈ ran ( ball β€˜ 𝐷 ) ( 𝑣 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑒 ) )
61 11 60 sylancom ⊒ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑒 βŠ† 𝑋 ) ∧ 𝑣 ∈ 𝑒 ) β†’ βˆƒ 𝑀 ∈ ran ( ball β€˜ 𝐷 ) ( 𝑣 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑒 ) )
62 61 ralrimiva ⊒ ( ( 𝑋 ∈ 𝑉 ∧ 𝑒 βŠ† 𝑋 ) β†’ βˆ€ 𝑣 ∈ 𝑒 βˆƒ 𝑀 ∈ ran ( ball β€˜ 𝐷 ) ( 𝑣 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑒 ) )
63 62 ex ⊒ ( 𝑋 ∈ 𝑉 β†’ ( 𝑒 βŠ† 𝑋 β†’ βˆ€ 𝑣 ∈ 𝑒 βˆƒ 𝑀 ∈ ran ( ball β€˜ 𝐷 ) ( 𝑣 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑒 ) ) )
64 63 pm4.71d ⊒ ( 𝑋 ∈ 𝑉 β†’ ( 𝑒 βŠ† 𝑋 ↔ ( 𝑒 βŠ† 𝑋 ∧ βˆ€ 𝑣 ∈ 𝑒 βˆƒ 𝑀 ∈ ran ( ball β€˜ 𝐷 ) ( 𝑣 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑒 ) ) ) )
65 7 64 bitr4d ⊒ ( 𝑋 ∈ 𝑉 β†’ ( 𝑒 ∈ ( MetOpen β€˜ 𝐷 ) ↔ 𝑒 βŠ† 𝑋 ) )
66 velpw ⊒ ( 𝑒 ∈ 𝒫 𝑋 ↔ 𝑒 βŠ† 𝑋 )
67 65 66 bitr4di ⊒ ( 𝑋 ∈ 𝑉 β†’ ( 𝑒 ∈ ( MetOpen β€˜ 𝐷 ) ↔ 𝑒 ∈ 𝒫 𝑋 ) )
68 67 eqrdv ⊒ ( 𝑋 ∈ 𝑉 β†’ ( MetOpen β€˜ 𝐷 ) = 𝒫 𝑋 )