Metamath Proof Explorer

Theorem metust

Description: The uniform structure generated by a metric D . (Contributed by Thierry Arnoux, 26-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Hypothesis metust.1 
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
Assertion metust 
|- ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( ( X X. X ) filGen F ) e. ( UnifOn ` X ) )

Proof

Step Hyp Ref Expression
1 metust.1 
 |-  F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
2 1 metustfbas 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> F e. ( fBas ` ( X X. X ) ) )
3 fgcl 
 |-  ( F e. ( fBas ` ( X X. X ) ) -> ( ( X X. X ) filGen F ) e. ( Fil ` ( X X. X ) ) )
4 filsspw 
 |-  ( ( ( X X. X ) filGen F ) e. ( Fil ` ( X X. X ) ) -> ( ( X X. X ) filGen F ) C_ ~P ( X X. X ) )
5 2 3 4 3syl 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( ( X X. X ) filGen F ) C_ ~P ( X X. X ) )
6 filtop 
 |-  ( ( ( X X. X ) filGen F ) e. ( Fil ` ( X X. X ) ) -> ( X X. X ) e. ( ( X X. X ) filGen F ) )
7 2 3 6 3syl 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( X X. X ) e. ( ( X X. X ) filGen F ) )
8 2 3 syl 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( ( X X. X ) filGen F ) e. ( Fil ` ( X X. X ) ) )
9 8 ad3antrrr 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ w e. ~P ( X X. X ) ) /\ v C_ w ) -> ( ( X X. X ) filGen F ) e. ( Fil ` ( X X. X ) ) )
10 simpllr 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ w e. ~P ( X X. X ) ) /\ v C_ w ) -> v e. ( ( X X. X ) filGen F ) )
11 simplr 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ w e. ~P ( X X. X ) ) /\ v C_ w ) -> w e. ~P ( X X. X ) )
12 11 elpwid 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ w e. ~P ( X X. X ) ) /\ v C_ w ) -> w C_ ( X X. X ) )
13 simpr 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ w e. ~P ( X X. X ) ) /\ v C_ w ) -> v C_ w )
14 filss 
 |-  ( ( ( ( X X. X ) filGen F ) e. ( Fil ` ( X X. X ) ) /\ ( v e. ( ( X X. X ) filGen F ) /\ w C_ ( X X. X ) /\ v C_ w ) ) -> w e. ( ( X X. X ) filGen F ) )
15 9 10 12 13 14 syl13anc 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ w e. ~P ( X X. X ) ) /\ v C_ w ) -> w e. ( ( X X. X ) filGen F ) )
16 15 ex 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ w e. ~P ( X X. X ) ) -> ( v C_ w -> w e. ( ( X X. X ) filGen F ) ) )
17 16 ralrimiva 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> A. w e. ~P ( X X. X ) ( v C_ w -> w e. ( ( X X. X ) filGen F ) ) )
18 8 ad2antrr 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ w e. ( ( X X. X ) filGen F ) ) -> ( ( X X. X ) filGen F ) e. ( Fil ` ( X X. X ) ) )
19 simplr 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ w e. ( ( X X. X ) filGen F ) ) -> v e. ( ( X X. X ) filGen F ) )
20 simpr 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ w e. ( ( X X. X ) filGen F ) ) -> w e. ( ( X X. X ) filGen F ) )
21 filin 
 |-  ( ( ( ( X X. X ) filGen F ) e. ( Fil ` ( X X. X ) ) /\ v e. ( ( X X. X ) filGen F ) /\ w e. ( ( X X. X ) filGen F ) ) -> ( v i^i w ) e. ( ( X X. X ) filGen F ) )
22 18 19 20 21 syl3anc 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ w e. ( ( X X. X ) filGen F ) ) -> ( v i^i w ) e. ( ( X X. X ) filGen F ) )
23 22 ralrimiva 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> A. w e. ( ( X X. X ) filGen F ) ( v i^i w ) e. ( ( X X. X ) filGen F ) )
24 1 metustid 
 |-  ( ( D e. ( PsMet ` X ) /\ u e. F ) -> ( _I |` X ) C_ u )
25 24 ad5ant24 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ u e. F ) /\ u C_ v ) -> ( _I |` X ) C_ u )
26 simpr 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ u e. F ) /\ u C_ v ) -> u C_ v )
27 25 26 sstrd 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ u e. F ) /\ u C_ v ) -> ( _I |` X ) C_ v )
28 elfg 
 |-  ( F e. ( fBas ` ( X X. X ) ) -> ( v e. ( ( X X. X ) filGen F ) <-> ( v C_ ( X X. X ) /\ E. u e. F u C_ v ) ) )
29 28 biimpa 
 |-  ( ( F e. ( fBas ` ( X X. X ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> ( v C_ ( X X. X ) /\ E. u e. F u C_ v ) )
30 29 simprd 
 |-  ( ( F e. ( fBas ` ( X X. X ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> E. u e. F u C_ v )
31 2 30 sylan 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> E. u e. F u C_ v )
32 27 31 r19.29a 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> ( _I |` X ) C_ v )
33 8 ad3antrrr 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ u e. F ) /\ u C_ v ) -> ( ( X X. X ) filGen F ) e. ( Fil ` ( X X. X ) ) )
34 2 adantr 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> F e. ( fBas ` ( X X. X ) ) )
35 ssfg 
 |-  ( F e. ( fBas ` ( X X. X ) ) -> F C_ ( ( X X. X ) filGen F ) )
36 34 35 syl 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> F C_ ( ( X X. X ) filGen F ) )
37 36 ad2antrr 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ u e. F ) /\ u C_ v ) -> F C_ ( ( X X. X ) filGen F ) )
38 simplr 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ u e. F ) /\ u C_ v ) -> u e. F )
39 37 38 sseldd 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ u e. F ) /\ u C_ v ) -> u e. ( ( X X. X ) filGen F ) )
40 29 simpld 
 |-  ( ( F e. ( fBas ` ( X X. X ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> v C_ ( X X. X ) )
41 2 40 sylan 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> v C_ ( X X. X ) )
42 41 ad2antrr 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ u e. F ) /\ u C_ v ) -> v C_ ( X X. X ) )
43 cnvss 
 |-  ( v C_ ( X X. X ) -> `' v C_ `' ( X X. X ) )
44 cnvxp 
 |-  `' ( X X. X ) = ( X X. X )
45 43 44 sseqtrdi 
 |-  ( v C_ ( X X. X ) -> `' v C_ ( X X. X ) )
46 42 45 syl 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ u e. F ) /\ u C_ v ) -> `' v C_ ( X X. X ) )
47 1 metustsym 
 |-  ( ( D e. ( PsMet ` X ) /\ u e. F ) -> `' u = u )
48 47 ad5ant24 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ u e. F ) /\ u C_ v ) -> `' u = u )
49 cnvss 
 |-  ( u C_ v -> `' u C_ `' v )
50 49 adantl 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ u e. F ) /\ u C_ v ) -> `' u C_ `' v )
51 48 50 eqsstrrd 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ u e. F ) /\ u C_ v ) -> u C_ `' v )
52 filss 
 |-  ( ( ( ( X X. X ) filGen F ) e. ( Fil ` ( X X. X ) ) /\ ( u e. ( ( X X. X ) filGen F ) /\ `' v C_ ( X X. X ) /\ u C_ `' v ) ) -> `' v e. ( ( X X. X ) filGen F ) )
53 33 39 46 51 52 syl13anc 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ u e. F ) /\ u C_ v ) -> `' v e. ( ( X X. X ) filGen F ) )
54 53 31 r19.29a 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> `' v e. ( ( X X. X ) filGen F ) )
55 1 metustexhalf 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ u e. F ) -> E. w e. F ( w o. w ) C_ u )
56 55 ad4ant13 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ u e. F ) /\ u C_ v ) -> E. w e. F ( w o. w ) C_ u )
57 r19.41v 
 |-  ( E. w e. F ( ( w o. w ) C_ u /\ u C_ v ) <-> ( E. w e. F ( w o. w ) C_ u /\ u C_ v ) )
58 sstr 
 |-  ( ( ( w o. w ) C_ u /\ u C_ v ) -> ( w o. w ) C_ v )
59 58 reximi 
 |-  ( E. w e. F ( ( w o. w ) C_ u /\ u C_ v ) -> E. w e. F ( w o. w ) C_ v )
60 57 59 sylbir 
 |-  ( ( E. w e. F ( w o. w ) C_ u /\ u C_ v ) -> E. w e. F ( w o. w ) C_ v )
61 56 60 sylancom 
 |-  ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ u e. F ) /\ u C_ v ) -> E. w e. F ( w o. w ) C_ v )
62 61 31 r19.29a 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> E. w e. F ( w o. w ) C_ v )
63 ssrexv 
 |-  ( F C_ ( ( X X. X ) filGen F ) -> ( E. w e. F ( w o. w ) C_ v -> E. w e. ( ( X X. X ) filGen F ) ( w o. w ) C_ v ) )
64 36 62 63 sylc 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> E. w e. ( ( X X. X ) filGen F ) ( w o. w ) C_ v )
65 32 54 64 3jca 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> ( ( _I |` X ) C_ v /\ `' v e. ( ( X X. X ) filGen F ) /\ E. w e. ( ( X X. X ) filGen F ) ( w o. w ) C_ v ) )
66 17 23 65 3jca 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> ( A. w e. ~P ( X X. X ) ( v C_ w -> w e. ( ( X X. X ) filGen F ) ) /\ A. w e. ( ( X X. X ) filGen F ) ( v i^i w ) e. ( ( X X. X ) filGen F ) /\ ( ( _I |` X ) C_ v /\ `' v e. ( ( X X. X ) filGen F ) /\ E. w e. ( ( X X. X ) filGen F ) ( w o. w ) C_ v ) ) )
67 66 ralrimiva 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> A. v e. ( ( X X. X ) filGen F ) ( A. w e. ~P ( X X. X ) ( v C_ w -> w e. ( ( X X. X ) filGen F ) ) /\ A. w e. ( ( X X. X ) filGen F ) ( v i^i w ) e. ( ( X X. X ) filGen F ) /\ ( ( _I |` X ) C_ v /\ `' v e. ( ( X X. X ) filGen F ) /\ E. w e. ( ( X X. X ) filGen F ) ( w o. w ) C_ v ) ) )
68 elfvex 
 |-  ( D e. ( PsMet ` X ) -> X e. _V )
69 68 adantl 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> X e. _V )
70 isust 
 |-  ( X e. _V -> ( ( ( X X. X ) filGen F ) e. ( UnifOn ` X ) <-> ( ( ( X X. X ) filGen F ) C_ ~P ( X X. X ) /\ ( X X. X ) e. ( ( X X. X ) filGen F ) /\ A. v e. ( ( X X. X ) filGen F ) ( A. w e. ~P ( X X. X ) ( v C_ w -> w e. ( ( X X. X ) filGen F ) ) /\ A. w e. ( ( X X. X ) filGen F ) ( v i^i w ) e. ( ( X X. X ) filGen F ) /\ ( ( _I |` X ) C_ v /\ `' v e. ( ( X X. X ) filGen F ) /\ E. w e. ( ( X X. X ) filGen F ) ( w o. w ) C_ v ) ) ) ) )
71 69 70 syl 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( ( ( X X. X ) filGen F ) e. ( UnifOn ` X ) <-> ( ( ( X X. X ) filGen F ) C_ ~P ( X X. X ) /\ ( X X. X ) e. ( ( X X. X ) filGen F ) /\ A. v e. ( ( X X. X ) filGen F ) ( A. w e. ~P ( X X. X ) ( v C_ w -> w e. ( ( X X. X ) filGen F ) ) /\ A. w e. ( ( X X. X ) filGen F ) ( v i^i w ) e. ( ( X X. X ) filGen F ) /\ ( ( _I |` X ) C_ v /\ `' v e. ( ( X X. X ) filGen F ) /\ E. w e. ( ( X X. X ) filGen F ) ( w o. w ) C_ v ) ) ) ) )
72 5 7 67 71 mpbir3and 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( ( X X. X ) filGen F ) e. ( UnifOn ` X ) )