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