Metamath Proof Explorer

Theorem cfilucfil

Description: Given a metric D and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil . (Contributed by Thierry Arnoux, 29-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Hypothesis metust.1 
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
Assertion cfilucfil 
|- ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) <-> ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )

Proof

Step Hyp Ref Expression
1 metust.1 
 |-  F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
2 1 metust 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( ( X X. X ) filGen F ) e. ( UnifOn ` X ) )
3 cfilufbas 
 |-  ( ( ( ( X X. X ) filGen F ) e. ( UnifOn ` X ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) -> C e. ( fBas ` X ) )
4 2 3 sylan 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) -> C e. ( fBas ` X ) )
5 simpllr 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> D e. ( PsMet ` X ) )
6 psmetf 
 |-  ( D e. ( PsMet ` X ) -> D : ( X X. X ) --> RR* )
7 ffun 
 |-  ( D : ( X X. X ) --> RR* -> Fun D )
8 5 6 7 3syl 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> Fun D )
9 2 ad2antrr 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> ( ( X X. X ) filGen F ) e. ( UnifOn ` X ) )
10 simplr 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) )
11 1 metustfbas 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> F e. ( fBas ` ( X X. X ) ) )
12 11 ad2antrr 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> F e. ( fBas ` ( X X. X ) ) )
13 cnvimass 
 |-  ( `' D " ( 0 [,) x ) ) C_ dom D
14 fdm 
 |-  ( D : ( X X. X ) --> RR* -> dom D = ( X X. X ) )
15 5 6 14 3syl 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> dom D = ( X X. X ) )
16 13 15 sseqtrid 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> ( `' D " ( 0 [,) x ) ) C_ ( X X. X ) )
17 simpr 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> x e. RR+ )
18 17 rphalfcld 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> ( x / 2 ) e. RR+ )
19 eqidd 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> ( `' D " ( 0 [,) ( x / 2 ) ) ) = ( `' D " ( 0 [,) ( x / 2 ) ) ) )
20 oveq2 
 |-  ( a = ( x / 2 ) -> ( 0 [,) a ) = ( 0 [,) ( x / 2 ) ) )
21 20 imaeq2d 
 |-  ( a = ( x / 2 ) -> ( `' D " ( 0 [,) a ) ) = ( `' D " ( 0 [,) ( x / 2 ) ) ) )
22 21 rspceeqv 
 |-  ( ( ( x / 2 ) e. RR+ /\ ( `' D " ( 0 [,) ( x / 2 ) ) ) = ( `' D " ( 0 [,) ( x / 2 ) ) ) ) -> E. a e. RR+ ( `' D " ( 0 [,) ( x / 2 ) ) ) = ( `' D " ( 0 [,) a ) ) )
23 18 19 22 syl2anc 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> E. a e. RR+ ( `' D " ( 0 [,) ( x / 2 ) ) ) = ( `' D " ( 0 [,) a ) ) )
24 1 metustel 
 |-  ( D e. ( PsMet ` X ) -> ( ( `' D " ( 0 [,) ( x / 2 ) ) ) e. F <-> E. a e. RR+ ( `' D " ( 0 [,) ( x / 2 ) ) ) = ( `' D " ( 0 [,) a ) ) ) )
25 24 biimpar 
 |-  ( ( D e. ( PsMet ` X ) /\ E. a e. RR+ ( `' D " ( 0 [,) ( x / 2 ) ) ) = ( `' D " ( 0 [,) a ) ) ) -> ( `' D " ( 0 [,) ( x / 2 ) ) ) e. F )
26 5 23 25 syl2anc 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> ( `' D " ( 0 [,) ( x / 2 ) ) ) e. F )
27 0xr 
 |-  0 e. RR*
28 27 a1i 
 |-  ( x e. RR+ -> 0 e. RR* )
29 rpxr 
 |-  ( x e. RR+ -> x e. RR* )
30 0le0 
 |-  0 <_ 0
31 30 a1i 
 |-  ( x e. RR+ -> 0 <_ 0 )
32 rpre 
 |-  ( x e. RR+ -> x e. RR )
33 32 rehalfcld 
 |-  ( x e. RR+ -> ( x / 2 ) e. RR )
34 rphalflt 
 |-  ( x e. RR+ -> ( x / 2 ) < x )
35 33 32 34 ltled 
 |-  ( x e. RR+ -> ( x / 2 ) <_ x )
36 icossico 
 |-  ( ( ( 0 e. RR* /\ x e. RR* ) /\ ( 0 <_ 0 /\ ( x / 2 ) <_ x ) ) -> ( 0 [,) ( x / 2 ) ) C_ ( 0 [,) x ) )
37 28 29 31 35 36 syl22anc 
 |-  ( x e. RR+ -> ( 0 [,) ( x / 2 ) ) C_ ( 0 [,) x ) )
38 imass2 
 |-  ( ( 0 [,) ( x / 2 ) ) C_ ( 0 [,) x ) -> ( `' D " ( 0 [,) ( x / 2 ) ) ) C_ ( `' D " ( 0 [,) x ) ) )
39 17 37 38 3syl 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> ( `' D " ( 0 [,) ( x / 2 ) ) ) C_ ( `' D " ( 0 [,) x ) ) )
40 sseq1 
 |-  ( w = ( `' D " ( 0 [,) ( x / 2 ) ) ) -> ( w C_ ( `' D " ( 0 [,) x ) ) <-> ( `' D " ( 0 [,) ( x / 2 ) ) ) C_ ( `' D " ( 0 [,) x ) ) ) )
41 40 rspcev 
 |-  ( ( ( `' D " ( 0 [,) ( x / 2 ) ) ) e. F /\ ( `' D " ( 0 [,) ( x / 2 ) ) ) C_ ( `' D " ( 0 [,) x ) ) ) -> E. w e. F w C_ ( `' D " ( 0 [,) x ) ) )
42 26 39 41 syl2anc 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> E. w e. F w C_ ( `' D " ( 0 [,) x ) ) )
43 elfg 
 |-  ( F e. ( fBas ` ( X X. X ) ) -> ( ( `' D " ( 0 [,) x ) ) e. ( ( X X. X ) filGen F ) <-> ( ( `' D " ( 0 [,) x ) ) C_ ( X X. X ) /\ E. w e. F w C_ ( `' D " ( 0 [,) x ) ) ) ) )
44 43 biimpar 
 |-  ( ( F e. ( fBas ` ( X X. X ) ) /\ ( ( `' D " ( 0 [,) x ) ) C_ ( X X. X ) /\ E. w e. F w C_ ( `' D " ( 0 [,) x ) ) ) ) -> ( `' D " ( 0 [,) x ) ) e. ( ( X X. X ) filGen F ) )
45 12 16 42 44 syl12anc 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> ( `' D " ( 0 [,) x ) ) e. ( ( X X. X ) filGen F ) )
46 cfiluexsm 
 |-  ( ( ( ( X X. X ) filGen F ) e. ( UnifOn ` X ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) /\ ( `' D " ( 0 [,) x ) ) e. ( ( X X. X ) filGen F ) ) -> E. y e. C ( y X. y ) C_ ( `' D " ( 0 [,) x ) ) )
47 9 10 45 46 syl3anc 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> E. y e. C ( y X. y ) C_ ( `' D " ( 0 [,) x ) ) )
48 funimass2 
 |-  ( ( Fun D /\ ( y X. y ) C_ ( `' D " ( 0 [,) x ) ) ) -> ( D " ( y X. y ) ) C_ ( 0 [,) x ) )
49 48 ex 
 |-  ( Fun D -> ( ( y X. y ) C_ ( `' D " ( 0 [,) x ) ) -> ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) )
50 49 reximdv 
 |-  ( Fun D -> ( E. y e. C ( y X. y ) C_ ( `' D " ( 0 [,) x ) ) -> E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) )
51 8 47 50 sylc 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) /\ x e. RR+ ) -> E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) )
52 51 ralrimiva 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) -> A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) )
53 4 52 jca 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) ) -> ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) )
54 simprl 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) -> C e. ( fBas ` X ) )
55 oveq2 
 |-  ( x = a -> ( 0 [,) x ) = ( 0 [,) a ) )
56 55 sseq2d 
 |-  ( x = a -> ( ( D " ( y X. y ) ) C_ ( 0 [,) x ) <-> ( D " ( y X. y ) ) C_ ( 0 [,) a ) ) )
57 56 rexbidv 
 |-  ( x = a -> ( E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) <-> E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) a ) ) )
58 simp-4r 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) )
59 58 simprd 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) )
60 simplr 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> a e. RR+ )
61 57 59 60 rspcdva 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) a ) )
62 nfv 
 |-  F/ y ( X =/= (/) /\ D e. ( PsMet ` X ) )
63 nfv 
 |-  F/ y C e. ( fBas ` X )
64 nfcv 
 |-  F/_ y RR+
65 nfre1 
 |-  F/ y E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x )
66 64 65 nfralw 
 |-  F/ y A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x )
67 63 66 nfan 
 |-  F/ y ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) )
68 62 67 nfan 
 |-  F/ y ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) )
69 nfv 
 |-  F/ y v e. ( ( X X. X ) filGen F )
70 68 69 nfan 
 |-  F/ y ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) )
71 nfv 
 |-  F/ y a e. RR+
72 70 71 nfan 
 |-  F/ y ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ )
73 nfv 
 |-  F/ y ( `' D " ( 0 [,) a ) ) C_ v
74 72 73 nfan 
 |-  F/ y ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v )
75 54 ad4antr 
 |-  ( ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) /\ y e. C ) -> C e. ( fBas ` X ) )
76 fbelss 
 |-  ( ( C e. ( fBas ` X ) /\ y e. C ) -> y C_ X )
77 75 76 sylancom 
 |-  ( ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) /\ y e. C ) -> y C_ X )
78 xpss12 
 |-  ( ( y C_ X /\ y C_ X ) -> ( y X. y ) C_ ( X X. X ) )
79 77 77 78 syl2anc 
 |-  ( ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) /\ y e. C ) -> ( y X. y ) C_ ( X X. X ) )
80 simp-6r 
 |-  ( ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) /\ y e. C ) -> D e. ( PsMet ` X ) )
81 80 6 14 3syl 
 |-  ( ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) /\ y e. C ) -> dom D = ( X X. X ) )
82 79 81 sseqtrrd 
 |-  ( ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) /\ y e. C ) -> ( y X. y ) C_ dom D )
83 82 ex 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> ( y e. C -> ( y X. y ) C_ dom D ) )
84 74 83 ralrimi 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> A. y e. C ( y X. y ) C_ dom D )
85 r19.29r 
 |-  ( ( E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) a ) /\ A. y e. C ( y X. y ) C_ dom D ) -> E. y e. C ( ( D " ( y X. y ) ) C_ ( 0 [,) a ) /\ ( y X. y ) C_ dom D ) )
86 sseqin2 
 |-  ( ( y X. y ) C_ dom D <-> ( dom D i^i ( y X. y ) ) = ( y X. y ) )
87 86 biimpi 
 |-  ( ( y X. y ) C_ dom D -> ( dom D i^i ( y X. y ) ) = ( y X. y ) )
88 87 adantl 
 |-  ( ( ( D " ( y X. y ) ) C_ ( 0 [,) a ) /\ ( y X. y ) C_ dom D ) -> ( dom D i^i ( y X. y ) ) = ( y X. y ) )
89 dminss 
 |-  ( dom D i^i ( y X. y ) ) C_ ( `' D " ( D " ( y X. y ) ) )
90 88 89 eqsstrrdi 
 |-  ( ( ( D " ( y X. y ) ) C_ ( 0 [,) a ) /\ ( y X. y ) C_ dom D ) -> ( y X. y ) C_ ( `' D " ( D " ( y X. y ) ) ) )
91 imass2 
 |-  ( ( D " ( y X. y ) ) C_ ( 0 [,) a ) -> ( `' D " ( D " ( y X. y ) ) ) C_ ( `' D " ( 0 [,) a ) ) )
92 91 adantr 
 |-  ( ( ( D " ( y X. y ) ) C_ ( 0 [,) a ) /\ ( y X. y ) C_ dom D ) -> ( `' D " ( D " ( y X. y ) ) ) C_ ( `' D " ( 0 [,) a ) ) )
93 90 92 sstrd 
 |-  ( ( ( D " ( y X. y ) ) C_ ( 0 [,) a ) /\ ( y X. y ) C_ dom D ) -> ( y X. y ) C_ ( `' D " ( 0 [,) a ) ) )
94 93 reximi 
 |-  ( E. y e. C ( ( D " ( y X. y ) ) C_ ( 0 [,) a ) /\ ( y X. y ) C_ dom D ) -> E. y e. C ( y X. y ) C_ ( `' D " ( 0 [,) a ) ) )
95 85 94 syl 
 |-  ( ( E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) a ) /\ A. y e. C ( y X. y ) C_ dom D ) -> E. y e. C ( y X. y ) C_ ( `' D " ( 0 [,) a ) ) )
96 61 84 95 syl2anc 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> E. y e. C ( y X. y ) C_ ( `' D " ( 0 [,) a ) ) )
97 r19.41v 
 |-  ( E. y e. C ( ( y X. y ) C_ ( `' D " ( 0 [,) a ) ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) <-> ( E. y e. C ( y X. y ) C_ ( `' D " ( 0 [,) a ) ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) )
98 sstr 
 |-  ( ( ( y X. y ) C_ ( `' D " ( 0 [,) a ) ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> ( y X. y ) C_ v )
99 98 reximi 
 |-  ( E. y e. C ( ( y X. y ) C_ ( `' D " ( 0 [,) a ) ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> E. y e. C ( y X. y ) C_ v )
100 97 99 sylbir 
 |-  ( ( E. y e. C ( y X. y ) C_ ( `' D " ( 0 [,) a ) ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> E. y e. C ( y X. y ) C_ v )
101 96 100 sylancom 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ a e. RR+ ) /\ ( `' D " ( 0 [,) a ) ) C_ v ) -> E. y e. C ( y X. y ) C_ v )
102 simp-5r 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ w e. F ) /\ w C_ v ) -> D e. ( PsMet ` X ) )
103 simplr 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ w e. F ) /\ w C_ v ) -> w e. F )
104 1 metustel 
 |-  ( D e. ( PsMet ` X ) -> ( w e. F <-> E. a e. RR+ w = ( `' D " ( 0 [,) a ) ) ) )
105 104 biimpa 
 |-  ( ( D e. ( PsMet ` X ) /\ w e. F ) -> E. a e. RR+ w = ( `' D " ( 0 [,) a ) ) )
106 102 103 105 syl2anc 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ w e. F ) /\ w C_ v ) -> E. a e. RR+ w = ( `' D " ( 0 [,) a ) ) )
107 r19.41v 
 |-  ( E. a e. RR+ ( w = ( `' D " ( 0 [,) a ) ) /\ w C_ v ) <-> ( E. a e. RR+ w = ( `' D " ( 0 [,) a ) ) /\ w C_ v ) )
108 sseq1 
 |-  ( w = ( `' D " ( 0 [,) a ) ) -> ( w C_ v <-> ( `' D " ( 0 [,) a ) ) C_ v ) )
109 108 biimpa 
 |-  ( ( w = ( `' D " ( 0 [,) a ) ) /\ w C_ v ) -> ( `' D " ( 0 [,) a ) ) C_ v )
110 109 reximi 
 |-  ( E. a e. RR+ ( w = ( `' D " ( 0 [,) a ) ) /\ w C_ v ) -> E. a e. RR+ ( `' D " ( 0 [,) a ) ) C_ v )
111 107 110 sylbir 
 |-  ( ( E. a e. RR+ w = ( `' D " ( 0 [,) a ) ) /\ w C_ v ) -> E. a e. RR+ ( `' D " ( 0 [,) a ) ) C_ v )
112 106 111 sylancom 
 |-  ( ( ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) /\ w e. F ) /\ w C_ v ) -> E. a e. RR+ ( `' D " ( 0 [,) a ) ) C_ v )
113 11 ad2antrr 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> F e. ( fBas ` ( X X. X ) ) )
114 elfg 
 |-  ( F e. ( fBas ` ( X X. X ) ) -> ( v e. ( ( X X. X ) filGen F ) <-> ( v C_ ( X X. X ) /\ E. w e. F w C_ v ) ) )
115 114 biimpa 
 |-  ( ( F e. ( fBas ` ( X X. X ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> ( v C_ ( X X. X ) /\ E. w e. F w C_ v ) )
116 113 115 sylancom 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> ( v C_ ( X X. X ) /\ E. w e. F w C_ v ) )
117 116 simprd 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> E. w e. F w C_ v )
118 112 117 r19.29a 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> E. a e. RR+ ( `' D " ( 0 [,) a ) ) C_ v )
119 101 118 r19.29a 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) /\ v e. ( ( X X. X ) filGen F ) ) -> E. y e. C ( y X. y ) C_ v )
120 119 ralrimiva 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) -> A. v e. ( ( X X. X ) filGen F ) E. y e. C ( y X. y ) C_ v )
121 2 adantr 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) -> ( ( X X. X ) filGen F ) e. ( UnifOn ` X ) )
122 iscfilu 
 |-  ( ( ( X X. X ) filGen F ) e. ( UnifOn ` X ) -> ( C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) <-> ( C e. ( fBas ` X ) /\ A. v e. ( ( X X. X ) filGen F ) E. y e. C ( y X. y ) C_ v ) ) )
123 121 122 syl 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) -> ( C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) <-> ( C e. ( fBas ` X ) /\ A. v e. ( ( X X. X ) filGen F ) E. y e. C ( y X. y ) C_ v ) ) )
124 54 120 123 mpbir2and 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) -> C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) )
125 53 124 impbida 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( C e. ( CauFilU ` ( ( X X. X ) filGen F ) ) <-> ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )