Metamath Proof Explorer

Theorem fbflim2

Description: A condition for a filter base B to converge to a point A . Use neighborhoods instead of open neighborhoods. Compare fbflim . (Contributed by FL, 4-Jul-2011) (Revised by Stefan O'Rear, 6-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 fbflim.3 
 |-  F = ( X filGen B )
2 1 fbflim 
 |-  ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ A. y e. J ( A e. y -> E. x e. B x C_ y ) ) ) )
3 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
4 3 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) -> J e. Top )
5 simpr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) -> A e. X )
6 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
7 6 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) -> X = U. J )
8 5 7 eleqtrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) -> A e. U. J )
9 eqid 
 |-  U. J = U. J
10 9 isneip 
 |-  ( ( J e. Top /\ A e. U. J ) -> ( n e. ( ( nei ` J ) ` { A } ) <-> ( n C_ U. J /\ E. y e. J ( A e. y /\ y C_ n ) ) ) )
11 4 8 10 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) -> ( n e. ( ( nei ` J ) ` { A } ) <-> ( n C_ U. J /\ E. y e. J ( A e. y /\ y C_ n ) ) ) )
12 simpr 
 |-  ( ( n C_ U. J /\ E. y e. J ( A e. y /\ y C_ n ) ) -> E. y e. J ( A e. y /\ y C_ n ) )
13 11 12 syl6bi 
 |-  ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) -> ( n e. ( ( nei ` J ) ` { A } ) -> E. y e. J ( A e. y /\ y C_ n ) ) )
14 r19.29 
 |-  ( ( A. y e. J ( A e. y -> E. x e. B x C_ y ) /\ E. y e. J ( A e. y /\ y C_ n ) ) -> E. y e. J ( ( A e. y -> E. x e. B x C_ y ) /\ ( A e. y /\ y C_ n ) ) )
15 pm3.45 
 |-  ( ( A e. y -> E. x e. B x C_ y ) -> ( ( A e. y /\ y C_ n ) -> ( E. x e. B x C_ y /\ y C_ n ) ) )
16 15 imp 
 |-  ( ( ( A e. y -> E. x e. B x C_ y ) /\ ( A e. y /\ y C_ n ) ) -> ( E. x e. B x C_ y /\ y C_ n ) )
17 sstr2 
 |-  ( x C_ y -> ( y C_ n -> x C_ n ) )
18 17 com12 
 |-  ( y C_ n -> ( x C_ y -> x C_ n ) )
19 18 reximdv 
 |-  ( y C_ n -> ( E. x e. B x C_ y -> E. x e. B x C_ n ) )
20 19 impcom 
 |-  ( ( E. x e. B x C_ y /\ y C_ n ) -> E. x e. B x C_ n )
21 16 20 syl 
 |-  ( ( ( A e. y -> E. x e. B x C_ y ) /\ ( A e. y /\ y C_ n ) ) -> E. x e. B x C_ n )
22 21 rexlimivw 
 |-  ( E. y e. J ( ( A e. y -> E. x e. B x C_ y ) /\ ( A e. y /\ y C_ n ) ) -> E. x e. B x C_ n )
23 14 22 syl 
 |-  ( ( A. y e. J ( A e. y -> E. x e. B x C_ y ) /\ E. y e. J ( A e. y /\ y C_ n ) ) -> E. x e. B x C_ n )
24 23 ex 
 |-  ( A. y e. J ( A e. y -> E. x e. B x C_ y ) -> ( E. y e. J ( A e. y /\ y C_ n ) -> E. x e. B x C_ n ) )
25 13 24 syl9 
 |-  ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) -> ( A. y e. J ( A e. y -> E. x e. B x C_ y ) -> ( n e. ( ( nei ` J ) ` { A } ) -> E. x e. B x C_ n ) ) )
26 25 ralrimdv 
 |-  ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) -> ( A. y e. J ( A e. y -> E. x e. B x C_ y ) -> A. n e. ( ( nei ` J ) ` { A } ) E. x e. B x C_ n ) )
27 4 adantr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ ( y e. J /\ A e. y ) ) -> J e. Top )
28 simprl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ ( y e. J /\ A e. y ) ) -> y e. J )
29 simprr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ ( y e. J /\ A e. y ) ) -> A e. y )
30 opnneip 
 |-  ( ( J e. Top /\ y e. J /\ A e. y ) -> y e. ( ( nei ` J ) ` { A } ) )
31 27 28 29 30 syl3anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ ( y e. J /\ A e. y ) ) -> y e. ( ( nei ` J ) ` { A } ) )
32 sseq2 
 |-  ( n = y -> ( x C_ n <-> x C_ y ) )
33 32 rexbidv 
 |-  ( n = y -> ( E. x e. B x C_ n <-> E. x e. B x C_ y ) )
34 33 rspcv 
 |-  ( y e. ( ( nei ` J ) ` { A } ) -> ( A. n e. ( ( nei ` J ) ` { A } ) E. x e. B x C_ n -> E. x e. B x C_ y ) )
35 31 34 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ ( y e. J /\ A e. y ) ) -> ( A. n e. ( ( nei ` J ) ` { A } ) E. x e. B x C_ n -> E. x e. B x C_ y ) )
36 35 expr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ y e. J ) -> ( A e. y -> ( A. n e. ( ( nei ` J ) ` { A } ) E. x e. B x C_ n -> E. x e. B x C_ y ) ) )
37 36 com23 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ y e. J ) -> ( A. n e. ( ( nei ` J ) ` { A } ) E. x e. B x C_ n -> ( A e. y -> E. x e. B x C_ y ) ) )
38 37 ralrimdva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) -> ( A. n e. ( ( nei ` J ) ` { A } ) E. x e. B x C_ n -> A. y e. J ( A e. y -> E. x e. B x C_ y ) ) )
39 26 38 impbid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) -> ( A. y e. J ( A e. y -> E. x e. B x C_ y ) <-> A. n e. ( ( nei ` J ) ` { A } ) E. x e. B x C_ n ) )
40 39 pm5.32da 
 |-  ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) -> ( ( A e. X /\ A. y e. J ( A e. y -> E. x e. B x C_ y ) ) <-> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) E. x e. B x C_ n ) ) )
41 2 40 bitrd 
 |-  ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ A. n e. ( ( nei ` J ) ` { A } ) E. x e. B x C_ n ) ) )