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 e. X , y e. X |-> if ( x = y , 0 , 1 ) )
Assertion dscopn 
|- ( X e. V -> ( MetOpen ` D ) = ~P X )

Proof

Step Hyp Ref Expression
1 dscmet.1 
 |-  D = ( x e. X , y e. X |-> if ( x = y , 0 , 1 ) )
2 1 dscmet 
 |-  ( X e. V -> D e. ( Met ` X ) )
3 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
4 2 3 syl 
 |-  ( X e. V -> D e. ( *Met ` X ) )
5 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
6 5 elmopn 
 |-  ( D e. ( *Met ` X ) -> ( u e. ( MetOpen ` D ) <-> ( u C_ X /\ A. v e. u E. w e. ran ( ball ` D ) ( v e. w /\ w C_ u ) ) ) )
7 4 6 syl 
 |-  ( X e. V -> ( u e. ( MetOpen ` D ) <-> ( u C_ X /\ A. v e. u E. w e. ran ( ball ` D ) ( v e. w /\ w C_ u ) ) ) )
8 simpll 
 |-  ( ( ( X e. V /\ u C_ X ) /\ v e. u ) -> X e. V )
9 ssel2 
 |-  ( ( u C_ X /\ v e. u ) -> v e. X )
10 9 adantll 
 |-  ( ( ( X e. V /\ u C_ X ) /\ v e. u ) -> v e. X )
11 8 10 jca 
 |-  ( ( ( X e. V /\ u C_ X ) /\ v e. u ) -> ( X e. V /\ v e. X ) )
12 velsn 
 |-  ( w e. { v } <-> w = v )
13 eleq1a 
 |-  ( v e. X -> ( w = v -> w e. X ) )
14 simpl 
 |-  ( ( w e. X /\ ( v D w ) < 1 ) -> w e. X )
15 14 a1i 
 |-  ( v e. X -> ( ( w e. X /\ ( v D w ) < 1 ) -> w e. 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 e. RR
19 1re 
 |-  1 e. RR
20 18 19 ifcli 
 |-  if ( v = w , 0 , 1 ) e. RR
21 20 elexi 
 |-  if ( v = w , 0 , 1 ) e. _V
22 17 1 21 ovmpoa 
 |-  ( ( v e. X /\ w e. X ) -> ( v D w ) = if ( v = w , 0 , 1 ) )
23 22 breq1d 
 |-  ( ( v e. X /\ w e. 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 e. X /\ w e. X ) -> ( w = v <-> ( v D w ) < 1 ) )
36 simpr 
 |-  ( ( v e. X /\ w e. X ) -> w e. X )
37 36 biantrurd 
 |-  ( ( v e. X /\ w e. X ) -> ( ( v D w ) < 1 <-> ( w e. X /\ ( v D w ) < 1 ) ) )
38 35 37 bitrd 
 |-  ( ( v e. X /\ w e. X ) -> ( w = v <-> ( w e. X /\ ( v D w ) < 1 ) ) )
39 38 ex 
 |-  ( v e. X -> ( w e. X -> ( w = v <-> ( w e. X /\ ( v D w ) < 1 ) ) ) )
40 13 15 39 pm5.21ndd 
 |-  ( v e. X -> ( w = v <-> ( w e. X /\ ( v D w ) < 1 ) ) )
41 40 adantl 
 |-  ( ( X e. V /\ v e. X ) -> ( w = v <-> ( w e. X /\ ( v D w ) < 1 ) ) )
42 1xr 
 |-  1 e. RR*
43 elbl 
 |-  ( ( D e. ( *Met ` X ) /\ v e. X /\ 1 e. RR* ) -> ( w e. ( v ( ball ` D ) 1 ) <-> ( w e. X /\ ( v D w ) < 1 ) ) )
44 42 43 mp3an3 
 |-  ( ( D e. ( *Met ` X ) /\ v e. X ) -> ( w e. ( v ( ball ` D ) 1 ) <-> ( w e. X /\ ( v D w ) < 1 ) ) )
45 4 44 sylan 
 |-  ( ( X e. V /\ v e. X ) -> ( w e. ( v ( ball ` D ) 1 ) <-> ( w e. X /\ ( v D w ) < 1 ) ) )
46 41 45 bitr4d 
 |-  ( ( X e. V /\ v e. X ) -> ( w = v <-> w e. ( v ( ball ` D ) 1 ) ) )
47 12 46 bitrid 
 |-  ( ( X e. V /\ v e. X ) -> ( w e. { v } <-> w e. ( v ( ball ` D ) 1 ) ) )
48 47 eqrdv 
 |-  ( ( X e. V /\ v e. X ) -> { v } = ( v ( ball ` D ) 1 ) )
49 blelrn 
 |-  ( ( D e. ( *Met ` X ) /\ v e. X /\ 1 e. RR* ) -> ( v ( ball ` D ) 1 ) e. ran ( ball ` D ) )
50 42 49 mp3an3 
 |-  ( ( D e. ( *Met ` X ) /\ v e. X ) -> ( v ( ball ` D ) 1 ) e. ran ( ball ` D ) )
51 4 50 sylan 
 |-  ( ( X e. V /\ v e. X ) -> ( v ( ball ` D ) 1 ) e. ran ( ball ` D ) )
52 48 51 eqeltrd 
 |-  ( ( X e. V /\ v e. X ) -> { v } e. ran ( ball ` D ) )
53 snssi 
 |-  ( v e. u -> { v } C_ u )
54 vsnid 
 |-  v e. { v }
55 53 54 jctil 
 |-  ( v e. u -> ( v e. { v } /\ { v } C_ u ) )
56 eleq2 
 |-  ( w = { v } -> ( v e. w <-> v e. { v } ) )
57 sseq1 
 |-  ( w = { v } -> ( w C_ u <-> { v } C_ u ) )
58 56 57 anbi12d 
 |-  ( w = { v } -> ( ( v e. w /\ w C_ u ) <-> ( v e. { v } /\ { v } C_ u ) ) )
59 58 rspcev 
 |-  ( ( { v } e. ran ( ball ` D ) /\ ( v e. { v } /\ { v } C_ u ) ) -> E. w e. ran ( ball ` D ) ( v e. w /\ w C_ u ) )
60 52 55 59 syl2an 
 |-  ( ( ( X e. V /\ v e. X ) /\ v e. u ) -> E. w e. ran ( ball ` D ) ( v e. w /\ w C_ u ) )
61 11 60 sylancom 
 |-  ( ( ( X e. V /\ u C_ X ) /\ v e. u ) -> E. w e. ran ( ball ` D ) ( v e. w /\ w C_ u ) )
62 61 ralrimiva 
 |-  ( ( X e. V /\ u C_ X ) -> A. v e. u E. w e. ran ( ball ` D ) ( v e. w /\ w C_ u ) )
63 62 ex 
 |-  ( X e. V -> ( u C_ X -> A. v e. u E. w e. ran ( ball ` D ) ( v e. w /\ w C_ u ) ) )
64 63 pm4.71d 
 |-  ( X e. V -> ( u C_ X <-> ( u C_ X /\ A. v e. u E. w e. ran ( ball ` D ) ( v e. w /\ w C_ u ) ) ) )
65 7 64 bitr4d 
 |-  ( X e. V -> ( u e. ( MetOpen ` D ) <-> u C_ X ) )
66 velpw 
 |-  ( u e. ~P X <-> u C_ X )
67 65 66 bitr4di 
 |-  ( X e. V -> ( u e. ( MetOpen ` D ) <-> u e. ~P X ) )
68 67 eqrdv 
 |-  ( X e. V -> ( MetOpen ` D ) = ~P X )