Metamath Proof Explorer

Theorem cfiluweak

Description: A Cauchy filter base is also a Cauchy filter base on any coarser uniform structure. (Contributed by Thierry Arnoux, 24-Jan-2018)

Ref Expression
Assertion cfiluweak 
|- ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) -> F e. ( CauFilU ` U ) )

Proof

Step Hyp Ref Expression
1 trust 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> ( U |`t ( A X. A ) ) e. ( UnifOn ` A ) )
2 iscfilu 
 |-  ( ( U |`t ( A X. A ) ) e. ( UnifOn ` A ) -> ( F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) <-> ( F e. ( fBas ` A ) /\ A. u e. ( U |`t ( A X. A ) ) E. a e. F ( a X. a ) C_ u ) ) )
3 2 biimpa 
 |-  ( ( ( U |`t ( A X. A ) ) e. ( UnifOn ` A ) /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) -> ( F e. ( fBas ` A ) /\ A. u e. ( U |`t ( A X. A ) ) E. a e. F ( a X. a ) C_ u ) )
4 1 3 stoic3 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) -> ( F e. ( fBas ` A ) /\ A. u e. ( U |`t ( A X. A ) ) E. a e. F ( a X. a ) C_ u ) )
5 4 simpld 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) -> F e. ( fBas ` A ) )
6 fbsspw 
 |-  ( F e. ( fBas ` A ) -> F C_ ~P A )
7 5 6 syl 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) -> F C_ ~P A )
8 simp2 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) -> A C_ X )
9 8 sspwd 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) -> ~P A C_ ~P X )
10 7 9 sstrd 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) -> F C_ ~P X )
11 simp1 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) -> U e. ( UnifOn ` X ) )
12 11 elfvexd 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) -> X e. _V )
13 fbasweak 
 |-  ( ( F e. ( fBas ` A ) /\ F C_ ~P X /\ X e. _V ) -> F e. ( fBas ` X ) )
14 5 10 12 13 syl3anc 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) -> F e. ( fBas ` X ) )
15 sseq2 
 |-  ( u = ( v i^i ( A X. A ) ) -> ( ( a X. a ) C_ u <-> ( a X. a ) C_ ( v i^i ( A X. A ) ) ) )
16 15 rexbidv 
 |-  ( u = ( v i^i ( A X. A ) ) -> ( E. a e. F ( a X. a ) C_ u <-> E. a e. F ( a X. a ) C_ ( v i^i ( A X. A ) ) ) )
17 4 simprd 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) -> A. u e. ( U |`t ( A X. A ) ) E. a e. F ( a X. a ) C_ u )
18 17 adantr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) /\ v e. U ) -> A. u e. ( U |`t ( A X. A ) ) E. a e. F ( a X. a ) C_ u )
19 11 adantr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) /\ v e. U ) -> U e. ( UnifOn ` X ) )
20 12 adantr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) /\ v e. U ) -> X e. _V )
21 8 adantr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) /\ v e. U ) -> A C_ X )
22 20 21 ssexd 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) /\ v e. U ) -> A e. _V )
23 22 22 xpexd 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) /\ v e. U ) -> ( A X. A ) e. _V )
24 simpr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) /\ v e. U ) -> v e. U )
25 elrestr 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( A X. A ) e. _V /\ v e. U ) -> ( v i^i ( A X. A ) ) e. ( U |`t ( A X. A ) ) )
26 19 23 24 25 syl3anc 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) /\ v e. U ) -> ( v i^i ( A X. A ) ) e. ( U |`t ( A X. A ) ) )
27 16 18 26 rspcdva 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) /\ v e. U ) -> E. a e. F ( a X. a ) C_ ( v i^i ( A X. A ) ) )
28 inss1 
 |-  ( v i^i ( A X. A ) ) C_ v
29 sstr 
 |-  ( ( ( a X. a ) C_ ( v i^i ( A X. A ) ) /\ ( v i^i ( A X. A ) ) C_ v ) -> ( a X. a ) C_ v )
30 28 29 mpan2 
 |-  ( ( a X. a ) C_ ( v i^i ( A X. A ) ) -> ( a X. a ) C_ v )
31 30 reximi 
 |-  ( E. a e. F ( a X. a ) C_ ( v i^i ( A X. A ) ) -> E. a e. F ( a X. a ) C_ v )
32 27 31 syl 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) /\ v e. U ) -> E. a e. F ( a X. a ) C_ v )
33 32 ralrimiva 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) -> A. v e. U E. a e. F ( a X. a ) C_ v )
34 iscfilu 
 |-  ( U e. ( UnifOn ` X ) -> ( F e. ( CauFilU ` U ) <-> ( F e. ( fBas ` X ) /\ A. v e. U E. a e. F ( a X. a ) C_ v ) ) )
35 34 3ad2ant1 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) -> ( F e. ( CauFilU ` U ) <-> ( F e. ( fBas ` X ) /\ A. v e. U E. a e. F ( a X. a ) C_ v ) ) )
36 14 33 35 mpbir2and 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X /\ F e. ( CauFilU ` ( U |`t ( A X. A ) ) ) ) -> F e. ( CauFilU ` U ) )