Metamath Proof Explorer

Theorem fgcfil

Description: The Cauchy filter condition for a filter base. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Assertion fgcfil 
|- ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` X ) ) -> ( ( X filGen B ) e. ( CauFil ` D ) <-> A. x e. RR+ E. y e. B A. z e. y A. w e. y ( z D w ) < x ) )

Proof

Step Hyp Ref Expression
1 cfili 
 |-  ( ( ( X filGen B ) e. ( CauFil ` D ) /\ x e. RR+ ) -> E. u e. ( X filGen B ) A. z e. u A. w e. u ( z D w ) < x )
2 1 adantll 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` X ) ) /\ ( X filGen B ) e. ( CauFil ` D ) ) /\ x e. RR+ ) -> E. u e. ( X filGen B ) A. z e. u A. w e. u ( z D w ) < x )
3 elfg 
 |-  ( B e. ( fBas ` X ) -> ( u e. ( X filGen B ) <-> ( u C_ X /\ E. y e. B y C_ u ) ) )
4 3 ad3antlr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` X ) ) /\ ( X filGen B ) e. ( CauFil ` D ) ) /\ x e. RR+ ) -> ( u e. ( X filGen B ) <-> ( u C_ X /\ E. y e. B y C_ u ) ) )
5 ssralv 
 |-  ( y C_ u -> ( A. w e. u ( z D w ) < x -> A. w e. y ( z D w ) < x ) )
6 5 ralimdv 
 |-  ( y C_ u -> ( A. z e. u A. w e. u ( z D w ) < x -> A. z e. u A. w e. y ( z D w ) < x ) )
7 ssralv 
 |-  ( y C_ u -> ( A. z e. u A. w e. y ( z D w ) < x -> A. z e. y A. w e. y ( z D w ) < x ) )
8 6 7 syldc 
 |-  ( A. z e. u A. w e. u ( z D w ) < x -> ( y C_ u -> A. z e. y A. w e. y ( z D w ) < x ) )
9 8 reximdv 
 |-  ( A. z e. u A. w e. u ( z D w ) < x -> ( E. y e. B y C_ u -> E. y e. B A. z e. y A. w e. y ( z D w ) < x ) )
10 9 com12 
 |-  ( E. y e. B y C_ u -> ( A. z e. u A. w e. u ( z D w ) < x -> E. y e. B A. z e. y A. w e. y ( z D w ) < x ) )
11 10 adantl 
 |-  ( ( u C_ X /\ E. y e. B y C_ u ) -> ( A. z e. u A. w e. u ( z D w ) < x -> E. y e. B A. z e. y A. w e. y ( z D w ) < x ) )
12 4 11 biimtrdi 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` X ) ) /\ ( X filGen B ) e. ( CauFil ` D ) ) /\ x e. RR+ ) -> ( u e. ( X filGen B ) -> ( A. z e. u A. w e. u ( z D w ) < x -> E. y e. B A. z e. y A. w e. y ( z D w ) < x ) ) )
13 12 rexlimdv 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` X ) ) /\ ( X filGen B ) e. ( CauFil ` D ) ) /\ x e. RR+ ) -> ( E. u e. ( X filGen B ) A. z e. u A. w e. u ( z D w ) < x -> E. y e. B A. z e. y A. w e. y ( z D w ) < x ) )
14 2 13 mpd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` X ) ) /\ ( X filGen B ) e. ( CauFil ` D ) ) /\ x e. RR+ ) -> E. y e. B A. z e. y A. w e. y ( z D w ) < x )
15 14 ralrimiva 
 |-  ( ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` X ) ) /\ ( X filGen B ) e. ( CauFil ` D ) ) -> A. x e. RR+ E. y e. B A. z e. y A. w e. y ( z D w ) < x )
16 15 ex 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` X ) ) -> ( ( X filGen B ) e. ( CauFil ` D ) -> A. x e. RR+ E. y e. B A. z e. y A. w e. y ( z D w ) < x ) )
17 ssfg 
 |-  ( B e. ( fBas ` X ) -> B C_ ( X filGen B ) )
18 17 adantl 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` X ) ) -> B C_ ( X filGen B ) )
19 ssrexv 
 |-  ( B C_ ( X filGen B ) -> ( E. y e. B A. z e. y A. w e. y ( z D w ) < x -> E. y e. ( X filGen B ) A. z e. y A. w e. y ( z D w ) < x ) )
20 19 ralimdv 
 |-  ( B C_ ( X filGen B ) -> ( A. x e. RR+ E. y e. B A. z e. y A. w e. y ( z D w ) < x -> A. x e. RR+ E. y e. ( X filGen B ) A. z e. y A. w e. y ( z D w ) < x ) )
21 18 20 syl 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` X ) ) -> ( A. x e. RR+ E. y e. B A. z e. y A. w e. y ( z D w ) < x -> A. x e. RR+ E. y e. ( X filGen B ) A. z e. y A. w e. y ( z D w ) < x ) )
22 fgcl 
 |-  ( B e. ( fBas ` X ) -> ( X filGen B ) e. ( Fil ` X ) )
23 22 adantl 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` X ) ) -> ( X filGen B ) e. ( Fil ` X ) )
24 21 23 jctild 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` X ) ) -> ( A. x e. RR+ E. y e. B A. z e. y A. w e. y ( z D w ) < x -> ( ( X filGen B ) e. ( Fil ` X ) /\ A. x e. RR+ E. y e. ( X filGen B ) A. z e. y A. w e. y ( z D w ) < x ) ) )
25 iscfil2 
 |-  ( D e. ( *Met ` X ) -> ( ( X filGen B ) e. ( CauFil ` D ) <-> ( ( X filGen B ) e. ( Fil ` X ) /\ A. x e. RR+ E. y e. ( X filGen B ) A. z e. y A. w e. y ( z D w ) < x ) ) )
26 25 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` X ) ) -> ( ( X filGen B ) e. ( CauFil ` D ) <-> ( ( X filGen B ) e. ( Fil ` X ) /\ A. x e. RR+ E. y e. ( X filGen B ) A. z e. y A. w e. y ( z D w ) < x ) ) )
27 24 26 sylibrd 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` X ) ) -> ( A. x e. RR+ E. y e. B A. z e. y A. w e. y ( z D w ) < x -> ( X filGen B ) e. ( CauFil ` D ) ) )
28 16 27 impbid 
 |-  ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` X ) ) -> ( ( X filGen B ) e. ( CauFil ` D ) <-> A. x e. RR+ E. y e. B A. z e. y A. w e. y ( z D w ) < x ) )