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 ) )