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