Metamath Proof Explorer

Theorem psmetutop

Description: The topology induced by a uniform structure generated by a metric D is generated by that metric's open balls. (Contributed by Thierry Arnoux, 6-Dec-2017) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion psmetutop 
|- ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( unifTop ` ( metUnif ` D ) ) = ( topGen ` ran ( ball ` D ) ) )

Proof

Step Hyp Ref Expression
1 metuust 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( metUnif ` D ) e. ( UnifOn ` X ) )
2 utopval 
 |-  ( ( metUnif ` D ) e. ( UnifOn ` X ) -> ( unifTop ` ( metUnif ` D ) ) = { a e. ~P X | A. x e. a E. v e. ( metUnif ` D ) ( v " { x } ) C_ a } )
3 1 2 syl 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( unifTop ` ( metUnif ` D ) ) = { a e. ~P X | A. x e. a E. v e. ( metUnif ` D ) ( v " { x } ) C_ a } )
4 3 eleq2d 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( a e. ( unifTop ` ( metUnif ` D ) ) <-> a e. { a e. ~P X | A. x e. a E. v e. ( metUnif ` D ) ( v " { x } ) C_ a } ) )
5 rabid 
 |-  ( a e. { a e. ~P X | A. x e. a E. v e. ( metUnif ` D ) ( v " { x } ) C_ a } <-> ( a e. ~P X /\ A. x e. a E. v e. ( metUnif ` D ) ( v " { x } ) C_ a ) )
6 4 5 bitrdi 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( a e. ( unifTop ` ( metUnif ` D ) ) <-> ( a e. ~P X /\ A. x e. a E. v e. ( metUnif ` D ) ( v " { x } ) C_ a ) ) )
7 6 biimpa 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) -> ( a e. ~P X /\ A. x e. a E. v e. ( metUnif ` D ) ( v " { x } ) C_ a ) )
8 7 simpld 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) -> a e. ~P X )
9 8 elpwid 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) -> a C_ X )
10 unirnblps 
 |-  ( D e. ( PsMet ` X ) -> U. ran ( ball ` D ) = X )
11 10 ad2antlr 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) -> U. ran ( ball ` D ) = X )
12 9 11 sseqtrrd 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) -> a C_ U. ran ( ball ` D ) )
13 simpr 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) /\ x e. a ) /\ v e. ( metUnif ` D ) ) /\ ( v " { x } ) C_ a ) -> ( v " { x } ) C_ a )
14 simp-5r 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) /\ x e. a ) /\ v e. ( metUnif ` D ) ) /\ ( v " { x } ) C_ a ) -> D e. ( PsMet ` X ) )
15 simplr 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) /\ x e. a ) /\ v e. ( metUnif ` D ) ) /\ ( v " { x } ) C_ a ) -> v e. ( metUnif ` D ) )
16 9 ad3antrrr 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) /\ x e. a ) /\ v e. ( metUnif ` D ) ) /\ ( v " { x } ) C_ a ) -> a C_ X )
17 simpllr 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) /\ x e. a ) /\ v e. ( metUnif ` D ) ) /\ ( v " { x } ) C_ a ) -> x e. a )
18 16 17 sseldd 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) /\ x e. a ) /\ v e. ( metUnif ` D ) ) /\ ( v " { x } ) C_ a ) -> x e. X )
19 metustbl 
 |-  ( ( D e. ( PsMet ` X ) /\ v e. ( metUnif ` D ) /\ x e. X ) -> E. b e. ran ( ball ` D ) ( x e. b /\ b C_ ( v " { x } ) ) )
20 14 15 18 19 syl3anc 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) /\ x e. a ) /\ v e. ( metUnif ` D ) ) /\ ( v " { x } ) C_ a ) -> E. b e. ran ( ball ` D ) ( x e. b /\ b C_ ( v " { x } ) ) )
21 sstr 
 |-  ( ( b C_ ( v " { x } ) /\ ( v " { x } ) C_ a ) -> b C_ a )
22 21 expcom 
 |-  ( ( v " { x } ) C_ a -> ( b C_ ( v " { x } ) -> b C_ a ) )
23 22 anim2d 
 |-  ( ( v " { x } ) C_ a -> ( ( x e. b /\ b C_ ( v " { x } ) ) -> ( x e. b /\ b C_ a ) ) )
24 23 reximdv 
 |-  ( ( v " { x } ) C_ a -> ( E. b e. ran ( ball ` D ) ( x e. b /\ b C_ ( v " { x } ) ) -> E. b e. ran ( ball ` D ) ( x e. b /\ b C_ a ) ) )
25 13 20 24 sylc 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) /\ x e. a ) /\ v e. ( metUnif ` D ) ) /\ ( v " { x } ) C_ a ) -> E. b e. ran ( ball ` D ) ( x e. b /\ b C_ a ) )
26 7 simprd 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) -> A. x e. a E. v e. ( metUnif ` D ) ( v " { x } ) C_ a )
27 26 r19.21bi 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) /\ x e. a ) -> E. v e. ( metUnif ` D ) ( v " { x } ) C_ a )
28 25 27 r19.29a 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) /\ x e. a ) -> E. b e. ran ( ball ` D ) ( x e. b /\ b C_ a ) )
29 28 ralrimiva 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) -> A. x e. a E. b e. ran ( ball ` D ) ( x e. b /\ b C_ a ) )
30 12 29 jca 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) -> ( a C_ U. ran ( ball ` D ) /\ A. x e. a E. b e. ran ( ball ` D ) ( x e. b /\ b C_ a ) ) )
31 fvex 
 |-  ( ball ` D ) e. _V
32 31 rnex 
 |-  ran ( ball ` D ) e. _V
33 eltg2 
 |-  ( ran ( ball ` D ) e. _V -> ( a e. ( topGen ` ran ( ball ` D ) ) <-> ( a C_ U. ran ( ball ` D ) /\ A. x e. a E. b e. ran ( ball ` D ) ( x e. b /\ b C_ a ) ) ) )
34 32 33 mp1i 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) -> ( a e. ( topGen ` ran ( ball ` D ) ) <-> ( a C_ U. ran ( ball ` D ) /\ A. x e. a E. b e. ran ( ball ` D ) ( x e. b /\ b C_ a ) ) ) )
35 30 34 mpbird 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( unifTop ` ( metUnif ` D ) ) ) -> a e. ( topGen ` ran ( ball ` D ) ) )
36 32 33 mp1i 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( a e. ( topGen ` ran ( ball ` D ) ) <-> ( a C_ U. ran ( ball ` D ) /\ A. x e. a E. b e. ran ( ball ` D ) ( x e. b /\ b C_ a ) ) ) )
37 36 biimpa 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) -> ( a C_ U. ran ( ball ` D ) /\ A. x e. a E. b e. ran ( ball ` D ) ( x e. b /\ b C_ a ) ) )
38 37 simpld 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) -> a C_ U. ran ( ball ` D ) )
39 10 ad2antlr 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) -> U. ran ( ball ` D ) = X )
40 38 39 sseqtrd 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) -> a C_ X )
41 elpwg 
 |-  ( a e. ( topGen ` ran ( ball ` D ) ) -> ( a e. ~P X <-> a C_ X ) )
42 41 adantl 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) -> ( a e. ~P X <-> a C_ X ) )
43 40 42 mpbird 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) -> a e. ~P X )
44 simpllr 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) /\ x e. a ) -> D e. ( PsMet ` X ) )
45 40 sselda 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) /\ x e. a ) -> x e. X )
46 37 simprd 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) -> A. x e. a E. b e. ran ( ball ` D ) ( x e. b /\ b C_ a ) )
47 46 r19.21bi 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) /\ x e. a ) -> E. b e. ran ( ball ` D ) ( x e. b /\ b C_ a ) )
48 blssexps 
 |-  ( ( D e. ( PsMet ` X ) /\ x e. X ) -> ( E. b e. ran ( ball ` D ) ( x e. b /\ b C_ a ) <-> E. d e. RR+ ( x ( ball ` D ) d ) C_ a ) )
49 44 45 48 syl2anc 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) /\ x e. a ) -> ( E. b e. ran ( ball ` D ) ( x e. b /\ b C_ a ) <-> E. d e. RR+ ( x ( ball ` D ) d ) C_ a ) )
50 47 49 mpbid 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) /\ x e. a ) -> E. d e. RR+ ( x ( ball ` D ) d ) C_ a )
51 blval2 
 |-  ( ( D e. ( PsMet ` X ) /\ x e. X /\ d e. RR+ ) -> ( x ( ball ` D ) d ) = ( ( `' D " ( 0 [,) d ) ) " { x } ) )
52 51 3expa 
 |-  ( ( ( D e. ( PsMet ` X ) /\ x e. X ) /\ d e. RR+ ) -> ( x ( ball ` D ) d ) = ( ( `' D " ( 0 [,) d ) ) " { x } ) )
53 52 sseq1d 
 |-  ( ( ( D e. ( PsMet ` X ) /\ x e. X ) /\ d e. RR+ ) -> ( ( x ( ball ` D ) d ) C_ a <-> ( ( `' D " ( 0 [,) d ) ) " { x } ) C_ a ) )
54 53 rexbidva 
 |-  ( ( D e. ( PsMet ` X ) /\ x e. X ) -> ( E. d e. RR+ ( x ( ball ` D ) d ) C_ a <-> E. d e. RR+ ( ( `' D " ( 0 [,) d ) ) " { x } ) C_ a ) )
55 54 biimpa 
 |-  ( ( ( D e. ( PsMet ` X ) /\ x e. X ) /\ E. d e. RR+ ( x ( ball ` D ) d ) C_ a ) -> E. d e. RR+ ( ( `' D " ( 0 [,) d ) ) " { x } ) C_ a )
56 44 45 50 55 syl21anc 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) /\ x e. a ) -> E. d e. RR+ ( ( `' D " ( 0 [,) d ) ) " { x } ) C_ a )
57 cnvexg 
 |-  ( D e. ( PsMet ` X ) -> `' D e. _V )
58 imaexg 
 |-  ( `' D e. _V -> ( `' D " ( 0 [,) d ) ) e. _V )
59 57 58 syl 
 |-  ( D e. ( PsMet ` X ) -> ( `' D " ( 0 [,) d ) ) e. _V )
60 59 ralrimivw 
 |-  ( D e. ( PsMet ` X ) -> A. d e. RR+ ( `' D " ( 0 [,) d ) ) e. _V )
61 eqid 
 |-  ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) ) = ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) )
62 imaeq1 
 |-  ( v = ( `' D " ( 0 [,) d ) ) -> ( v " { x } ) = ( ( `' D " ( 0 [,) d ) ) " { x } ) )
63 62 sseq1d 
 |-  ( v = ( `' D " ( 0 [,) d ) ) -> ( ( v " { x } ) C_ a <-> ( ( `' D " ( 0 [,) d ) ) " { x } ) C_ a ) )
64 61 63 rexrnmptw 
 |-  ( A. d e. RR+ ( `' D " ( 0 [,) d ) ) e. _V -> ( E. v e. ran ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) ) ( v " { x } ) C_ a <-> E. d e. RR+ ( ( `' D " ( 0 [,) d ) ) " { x } ) C_ a ) )
65 44 60 64 3syl 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) /\ x e. a ) -> ( E. v e. ran ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) ) ( v " { x } ) C_ a <-> E. d e. RR+ ( ( `' D " ( 0 [,) d ) ) " { x } ) C_ a ) )
66 56 65 mpbird 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) /\ x e. a ) -> E. v e. ran ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) ) ( v " { x } ) C_ a )
67 oveq2 
 |-  ( d = e -> ( 0 [,) d ) = ( 0 [,) e ) )
68 67 imaeq2d 
 |-  ( d = e -> ( `' D " ( 0 [,) d ) ) = ( `' D " ( 0 [,) e ) ) )
69 68 cbvmptv 
 |-  ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) ) = ( e e. RR+ |-> ( `' D " ( 0 [,) e ) ) )
70 69 rneqi 
 |-  ran ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) ) = ran ( e e. RR+ |-> ( `' D " ( 0 [,) e ) ) )
71 70 metustfbas 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ran ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) ) e. ( fBas ` ( X X. X ) ) )
72 ssfg 
 |-  ( ran ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) ) e. ( fBas ` ( X X. X ) ) -> ran ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) ) C_ ( ( X X. X ) filGen ran ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) ) ) )
73 71 72 syl 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ran ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) ) C_ ( ( X X. X ) filGen ran ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) ) ) )
74 metuval 
 |-  ( D e. ( PsMet ` X ) -> ( metUnif ` D ) = ( ( X X. X ) filGen ran ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) ) ) )
75 74 adantl 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( metUnif ` D ) = ( ( X X. X ) filGen ran ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) ) ) )
76 73 75 sseqtrrd 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ran ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) ) C_ ( metUnif ` D ) )
77 ssrexv 
 |-  ( ran ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) ) C_ ( metUnif ` D ) -> ( E. v e. ran ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) ) ( v " { x } ) C_ a -> E. v e. ( metUnif ` D ) ( v " { x } ) C_ a ) )
78 76 77 syl 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( E. v e. ran ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) ) ( v " { x } ) C_ a -> E. v e. ( metUnif ` D ) ( v " { x } ) C_ a ) )
79 78 ad2antrr 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) /\ x e. a ) -> ( E. v e. ran ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) ) ( v " { x } ) C_ a -> E. v e. ( metUnif ` D ) ( v " { x } ) C_ a ) )
80 66 79 mpd 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) /\ x e. a ) -> E. v e. ( metUnif ` D ) ( v " { x } ) C_ a )
81 80 ralrimiva 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) -> A. x e. a E. v e. ( metUnif ` D ) ( v " { x } ) C_ a )
82 43 81 jca 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) -> ( a e. ~P X /\ A. x e. a E. v e. ( metUnif ` D ) ( v " { x } ) C_ a ) )
83 6 biimpar 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( a e. ~P X /\ A. x e. a E. v e. ( metUnif ` D ) ( v " { x } ) C_ a ) ) -> a e. ( unifTop ` ( metUnif ` D ) ) )
84 82 83 syldan 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ a e. ( topGen ` ran ( ball ` D ) ) ) -> a e. ( unifTop ` ( metUnif ` D ) ) )
85 35 84 impbida 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( a e. ( unifTop ` ( metUnif ` D ) ) <-> a e. ( topGen ` ran ( ball ` D ) ) ) )
86 85 eqrdv 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( unifTop ` ( metUnif ` D ) ) = ( topGen ` ran ( ball ` D ) ) )