Metamath Proof Explorer

Theorem fbflim

Description: A condition for a filter to converge to a point involving one of its bases. (Contributed by Jeff Hankins, 4-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Hypothesis fbflim.3 
|- F = ( X filGen B )
Assertion fbflim 
|- ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ A. x e. J ( A e. x -> E. y e. B y C_ x ) ) ) )

Proof

Step Hyp Ref Expression
1 fbflim.3 
 |-  F = ( X filGen B )
2 fgcl 
 |-  ( B e. ( fBas ` X ) -> ( X filGen B ) e. ( Fil ` X ) )
3 1 2 eqeltrid 
 |-  ( B e. ( fBas ` X ) -> F e. ( Fil ` X ) )
4 flimopn 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ A. x e. J ( A e. x -> x e. F ) ) ) )
5 3 4 sylan2 
 |-  ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ A. x e. J ( A e. x -> x e. F ) ) ) )
6 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ x e. J ) -> x C_ X )
7 6 ad4ant14 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ x e. J ) -> x C_ X )
8 1 eleq2i 
 |-  ( x e. F <-> x e. ( X filGen B ) )
9 elfg 
 |-  ( B e. ( fBas ` X ) -> ( x e. ( X filGen B ) <-> ( x C_ X /\ E. y e. B y C_ x ) ) )
10 9 ad3antlr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ x e. J ) -> ( x e. ( X filGen B ) <-> ( x C_ X /\ E. y e. B y C_ x ) ) )
11 8 10 syl5bb 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ x e. J ) -> ( x e. F <-> ( x C_ X /\ E. y e. B y C_ x ) ) )
12 7 11 mpbirand 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ x e. J ) -> ( x e. F <-> E. y e. B y C_ x ) )
13 12 imbi2d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ x e. J ) -> ( ( A e. x -> x e. F ) <-> ( A e. x -> E. y e. B y C_ x ) ) )
14 13 ralbidva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) -> ( A. x e. J ( A e. x -> x e. F ) <-> A. x e. J ( A e. x -> E. y e. B y C_ x ) ) )
15 14 pm5.32da 
 |-  ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) -> ( ( A e. X /\ A. x e. J ( A e. x -> x e. F ) ) <-> ( A e. X /\ A. x e. J ( A e. x -> E. y e. B y C_ x ) ) ) )
16 5 15 bitrd 
 |-  ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ A. x e. J ( A e. x -> E. y e. B y C_ x ) ) ) )