Metamath Proof Explorer

Theorem metuel2

Description: Elementhood in the uniform structure generated by a metric D (Contributed by Thierry Arnoux, 24-Jan-2018) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Hypothesis metuel2.u 
|- U = ( metUnif ` D )
Assertion metuel2 
|- ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( V e. U <-> ( V C_ ( X X. X ) /\ E. d e. RR+ A. x e. X A. y e. X ( ( x D y ) < d -> x V y ) ) ) )

Proof

Step Hyp Ref Expression
1 metuel2.u 
 |-  U = ( metUnif ` D )
2 1 eleq2i 
 |-  ( V e. U <-> V e. ( metUnif ` D ) )
3 2 a1i 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( V e. U <-> V e. ( metUnif ` D ) ) )
4 metuel 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( V e. ( metUnif ` D ) <-> ( V C_ ( X X. X ) /\ E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ V ) ) )
5 oveq2 
 |-  ( a = d -> ( 0 [,) a ) = ( 0 [,) d ) )
6 5 imaeq2d 
 |-  ( a = d -> ( `' D " ( 0 [,) a ) ) = ( `' D " ( 0 [,) d ) ) )
7 6 cbvmptv 
 |-  ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) = ( d e. RR+ |-> ( `' D " ( 0 [,) d ) ) )
8 7 elrnmpt 
 |-  ( w e. _V -> ( w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) <-> E. d e. RR+ w = ( `' D " ( 0 [,) d ) ) ) )
9 8 elv 
 |-  ( w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) <-> E. d e. RR+ w = ( `' D " ( 0 [,) d ) ) )
10 9 anbi1i 
 |-  ( ( w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) /\ w C_ V ) <-> ( E. d e. RR+ w = ( `' D " ( 0 [,) d ) ) /\ w C_ V ) )
11 r19.41v 
 |-  ( E. d e. RR+ ( w = ( `' D " ( 0 [,) d ) ) /\ w C_ V ) <-> ( E. d e. RR+ w = ( `' D " ( 0 [,) d ) ) /\ w C_ V ) )
12 10 11 bitr4i 
 |-  ( ( w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) /\ w C_ V ) <-> E. d e. RR+ ( w = ( `' D " ( 0 [,) d ) ) /\ w C_ V ) )
13 12 exbii 
 |-  ( E. w ( w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) /\ w C_ V ) <-> E. w E. d e. RR+ ( w = ( `' D " ( 0 [,) d ) ) /\ w C_ V ) )
14 df-rex 
 |-  ( E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ V <-> E. w ( w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) /\ w C_ V ) )
15 rexcom4 
 |-  ( E. d e. RR+ E. w ( w = ( `' D " ( 0 [,) d ) ) /\ w C_ V ) <-> E. w E. d e. RR+ ( w = ( `' D " ( 0 [,) d ) ) /\ w C_ V ) )
16 13 14 15 3bitr4i 
 |-  ( E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ V <-> E. d e. RR+ E. w ( w = ( `' D " ( 0 [,) d ) ) /\ w C_ V ) )
17 cnvexg 
 |-  ( D e. ( PsMet ` X ) -> `' D e. _V )
18 imaexg 
 |-  ( `' D e. _V -> ( `' D " ( 0 [,) d ) ) e. _V )
19 sseq1 
 |-  ( w = ( `' D " ( 0 [,) d ) ) -> ( w C_ V <-> ( `' D " ( 0 [,) d ) ) C_ V ) )
20 19 ceqsexgv 
 |-  ( ( `' D " ( 0 [,) d ) ) e. _V -> ( E. w ( w = ( `' D " ( 0 [,) d ) ) /\ w C_ V ) <-> ( `' D " ( 0 [,) d ) ) C_ V ) )
21 17 18 20 3syl 
 |-  ( D e. ( PsMet ` X ) -> ( E. w ( w = ( `' D " ( 0 [,) d ) ) /\ w C_ V ) <-> ( `' D " ( 0 [,) d ) ) C_ V ) )
22 21 rexbidv 
 |-  ( D e. ( PsMet ` X ) -> ( E. d e. RR+ E. w ( w = ( `' D " ( 0 [,) d ) ) /\ w C_ V ) <-> E. d e. RR+ ( `' D " ( 0 [,) d ) ) C_ V ) )
23 22 adantr 
 |-  ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) -> ( E. d e. RR+ E. w ( w = ( `' D " ( 0 [,) d ) ) /\ w C_ V ) <-> E. d e. RR+ ( `' D " ( 0 [,) d ) ) C_ V ) )
24 16 23 syl5bb 
 |-  ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) -> ( E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ V <-> E. d e. RR+ ( `' D " ( 0 [,) d ) ) C_ V ) )
25 cnvimass 
 |-  ( `' D " ( 0 [,) d ) ) C_ dom D
26 simpll 
 |-  ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) -> D e. ( PsMet ` X ) )
27 psmetf 
 |-  ( D e. ( PsMet ` X ) -> D : ( X X. X ) --> RR* )
28 fdm 
 |-  ( D : ( X X. X ) --> RR* -> dom D = ( X X. X ) )
29 26 27 28 3syl 
 |-  ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) -> dom D = ( X X. X ) )
30 25 29 sseqtrid 
 |-  ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) -> ( `' D " ( 0 [,) d ) ) C_ ( X X. X ) )
31 ssrel2 
 |-  ( ( `' D " ( 0 [,) d ) ) C_ ( X X. X ) -> ( ( `' D " ( 0 [,) d ) ) C_ V <-> A. x e. X A. y e. X ( <. x , y >. e. ( `' D " ( 0 [,) d ) ) -> <. x , y >. e. V ) ) )
32 30 31 syl 
 |-  ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) -> ( ( `' D " ( 0 [,) d ) ) C_ V <-> A. x e. X A. y e. X ( <. x , y >. e. ( `' D " ( 0 [,) d ) ) -> <. x , y >. e. V ) ) )
33 simplr 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) /\ x e. X ) /\ y e. X ) -> x e. X )
34 simpr 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) /\ x e. X ) /\ y e. X ) -> y e. X )
35 33 34 opelxpd 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) /\ x e. X ) /\ y e. X ) -> <. x , y >. e. ( X X. X ) )
36 35 biantrurd 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) /\ x e. X ) /\ y e. X ) -> ( ( D ` <. x , y >. ) e. ( 0 [,) d ) <-> ( <. x , y >. e. ( X X. X ) /\ ( D ` <. x , y >. ) e. ( 0 [,) d ) ) ) )
37 psmetcl 
 |-  ( ( D e. ( PsMet ` X ) /\ x e. X /\ y e. X ) -> ( x D y ) e. RR* )
38 37 ad5ant145 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) /\ x e. X ) /\ y e. X ) -> ( x D y ) e. RR* )
39 38 3biant1d 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) /\ x e. X ) /\ y e. X ) -> ( ( 0 <_ ( x D y ) /\ ( x D y ) < d ) <-> ( ( x D y ) e. RR* /\ 0 <_ ( x D y ) /\ ( x D y ) < d ) ) )
40 psmetge0 
 |-  ( ( D e. ( PsMet ` X ) /\ x e. X /\ y e. X ) -> 0 <_ ( x D y ) )
41 40 biantrurd 
 |-  ( ( D e. ( PsMet ` X ) /\ x e. X /\ y e. X ) -> ( ( x D y ) < d <-> ( 0 <_ ( x D y ) /\ ( x D y ) < d ) ) )
42 41 ad5ant145 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) /\ x e. X ) /\ y e. X ) -> ( ( x D y ) < d <-> ( 0 <_ ( x D y ) /\ ( x D y ) < d ) ) )
43 0xr 
 |-  0 e. RR*
44 simpllr 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) /\ x e. X ) /\ y e. X ) -> d e. RR+ )
45 44 rpxrd 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) /\ x e. X ) /\ y e. X ) -> d e. RR* )
46 elico1 
 |-  ( ( 0 e. RR* /\ d e. RR* ) -> ( ( x D y ) e. ( 0 [,) d ) <-> ( ( x D y ) e. RR* /\ 0 <_ ( x D y ) /\ ( x D y ) < d ) ) )
47 43 45 46 sylancr 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) /\ x e. X ) /\ y e. X ) -> ( ( x D y ) e. ( 0 [,) d ) <-> ( ( x D y ) e. RR* /\ 0 <_ ( x D y ) /\ ( x D y ) < d ) ) )
48 39 42 47 3bitr4d 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) /\ x e. X ) /\ y e. X ) -> ( ( x D y ) < d <-> ( x D y ) e. ( 0 [,) d ) ) )
49 df-ov 
 |-  ( x D y ) = ( D ` <. x , y >. )
50 49 eleq1i 
 |-  ( ( x D y ) e. ( 0 [,) d ) <-> ( D ` <. x , y >. ) e. ( 0 [,) d ) )
51 48 50 bitrdi 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) /\ x e. X ) /\ y e. X ) -> ( ( x D y ) < d <-> ( D ` <. x , y >. ) e. ( 0 [,) d ) ) )
52 simp-4l 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) /\ x e. X ) /\ y e. X ) -> D e. ( PsMet ` X ) )
53 ffn 
 |-  ( D : ( X X. X ) --> RR* -> D Fn ( X X. X ) )
54 elpreima 
 |-  ( D Fn ( X X. X ) -> ( <. x , y >. e. ( `' D " ( 0 [,) d ) ) <-> ( <. x , y >. e. ( X X. X ) /\ ( D ` <. x , y >. ) e. ( 0 [,) d ) ) ) )
55 52 27 53 54 4syl 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) /\ x e. X ) /\ y e. X ) -> ( <. x , y >. e. ( `' D " ( 0 [,) d ) ) <-> ( <. x , y >. e. ( X X. X ) /\ ( D ` <. x , y >. ) e. ( 0 [,) d ) ) ) )
56 36 51 55 3bitr4d 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) /\ x e. X ) /\ y e. X ) -> ( ( x D y ) < d <-> <. x , y >. e. ( `' D " ( 0 [,) d ) ) ) )
57 56 anasss 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> ( ( x D y ) < d <-> <. x , y >. e. ( `' D " ( 0 [,) d ) ) ) )
58 df-br 
 |-  ( x V y <-> <. x , y >. e. V )
59 58 a1i 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> ( x V y <-> <. x , y >. e. V ) )
60 57 59 imbi12d 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) /\ ( x e. X /\ y e. X ) ) -> ( ( ( x D y ) < d -> x V y ) <-> ( <. x , y >. e. ( `' D " ( 0 [,) d ) ) -> <. x , y >. e. V ) ) )
61 60 2ralbidva 
 |-  ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) -> ( A. x e. X A. y e. X ( ( x D y ) < d -> x V y ) <-> A. x e. X A. y e. X ( <. x , y >. e. ( `' D " ( 0 [,) d ) ) -> <. x , y >. e. V ) ) )
62 32 61 bitr4d 
 |-  ( ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) /\ d e. RR+ ) -> ( ( `' D " ( 0 [,) d ) ) C_ V <-> A. x e. X A. y e. X ( ( x D y ) < d -> x V y ) ) )
63 62 rexbidva 
 |-  ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) -> ( E. d e. RR+ ( `' D " ( 0 [,) d ) ) C_ V <-> E. d e. RR+ A. x e. X A. y e. X ( ( x D y ) < d -> x V y ) ) )
64 24 63 bitrd 
 |-  ( ( D e. ( PsMet ` X ) /\ V C_ ( X X. X ) ) -> ( E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ V <-> E. d e. RR+ A. x e. X A. y e. X ( ( x D y ) < d -> x V y ) ) )
65 64 pm5.32da 
 |-  ( D e. ( PsMet ` X ) -> ( ( V C_ ( X X. X ) /\ E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ V ) <-> ( V C_ ( X X. X ) /\ E. d e. RR+ A. x e. X A. y e. X ( ( x D y ) < d -> x V y ) ) ) )
66 65 adantl 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( ( V C_ ( X X. X ) /\ E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ V ) <-> ( V C_ ( X X. X ) /\ E. d e. RR+ A. x e. X A. y e. X ( ( x D y ) < d -> x V y ) ) ) )
67 3 4 66 3bitrd 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( V e. U <-> ( V C_ ( X X. X ) /\ E. d e. RR+ A. x e. X A. y e. X ( ( x D y ) < d -> x V y ) ) ) )