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