Step |
Hyp |
Ref |
Expression |
1 |
|
flimtop |
|- ( A e. ( J fLim F ) -> J e. Top ) |
2 |
|
eqid |
|- U. J = U. J |
3 |
2
|
flimelbas |
|- ( A e. ( J fLim F ) -> A e. U. J ) |
4 |
3
|
snssd |
|- ( A e. ( J fLim F ) -> { A } C_ U. J ) |
5 |
2
|
clsss3 |
|- ( ( J e. Top /\ { A } C_ U. J ) -> ( ( cls ` J ) ` { A } ) C_ U. J ) |
6 |
1 4 5
|
syl2anc |
|- ( A e. ( J fLim F ) -> ( ( cls ` J ) ` { A } ) C_ U. J ) |
7 |
6
|
sselda |
|- ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> x e. U. J ) |
8 |
|
simpll |
|- ( ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) /\ ( y e. J /\ x e. y ) ) -> A e. ( J fLim F ) ) |
9 |
8 1
|
syl |
|- ( ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) /\ ( y e. J /\ x e. y ) ) -> J e. Top ) |
10 |
|
simprl |
|- ( ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) /\ ( y e. J /\ x e. y ) ) -> y e. J ) |
11 |
1
|
adantr |
|- ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> J e. Top ) |
12 |
4
|
adantr |
|- ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> { A } C_ U. J ) |
13 |
|
simpr |
|- ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> x e. ( ( cls ` J ) ` { A } ) ) |
14 |
11 12 13
|
3jca |
|- ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> ( J e. Top /\ { A } C_ U. J /\ x e. ( ( cls ` J ) ` { A } ) ) ) |
15 |
2
|
clsndisj |
|- ( ( ( J e. Top /\ { A } C_ U. J /\ x e. ( ( cls ` J ) ` { A } ) ) /\ ( y e. J /\ x e. y ) ) -> ( y i^i { A } ) =/= (/) ) |
16 |
|
disjsn |
|- ( ( y i^i { A } ) = (/) <-> -. A e. y ) |
17 |
16
|
necon2abii |
|- ( A e. y <-> ( y i^i { A } ) =/= (/) ) |
18 |
15 17
|
sylibr |
|- ( ( ( J e. Top /\ { A } C_ U. J /\ x e. ( ( cls ` J ) ` { A } ) ) /\ ( y e. J /\ x e. y ) ) -> A e. y ) |
19 |
14 18
|
sylan |
|- ( ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) /\ ( y e. J /\ x e. y ) ) -> A e. y ) |
20 |
|
opnneip |
|- ( ( J e. Top /\ y e. J /\ A e. y ) -> y e. ( ( nei ` J ) ` { A } ) ) |
21 |
9 10 19 20
|
syl3anc |
|- ( ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) /\ ( y e. J /\ x e. y ) ) -> y e. ( ( nei ` J ) ` { A } ) ) |
22 |
|
flimnei |
|- ( ( A e. ( J fLim F ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> y e. F ) |
23 |
8 21 22
|
syl2anc |
|- ( ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) /\ ( y e. J /\ x e. y ) ) -> y e. F ) |
24 |
23
|
expr |
|- ( ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) /\ y e. J ) -> ( x e. y -> y e. F ) ) |
25 |
24
|
ralrimiva |
|- ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> A. y e. J ( x e. y -> y e. F ) ) |
26 |
|
toptopon2 |
|- ( J e. Top <-> J e. ( TopOn ` U. J ) ) |
27 |
11 26
|
sylib |
|- ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> J e. ( TopOn ` U. J ) ) |
28 |
2
|
flimfil |
|- ( A e. ( J fLim F ) -> F e. ( Fil ` U. J ) ) |
29 |
28
|
adantr |
|- ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> F e. ( Fil ` U. J ) ) |
30 |
|
flimopn |
|- ( ( J e. ( TopOn ` U. J ) /\ F e. ( Fil ` U. J ) ) -> ( x e. ( J fLim F ) <-> ( x e. U. J /\ A. y e. J ( x e. y -> y e. F ) ) ) ) |
31 |
27 29 30
|
syl2anc |
|- ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> ( x e. ( J fLim F ) <-> ( x e. U. J /\ A. y e. J ( x e. y -> y e. F ) ) ) ) |
32 |
7 25 31
|
mpbir2and |
|- ( ( A e. ( J fLim F ) /\ x e. ( ( cls ` J ) ` { A } ) ) -> x e. ( J fLim F ) ) |
33 |
32
|
ex |
|- ( A e. ( J fLim F ) -> ( x e. ( ( cls ` J ) ` { A } ) -> x e. ( J fLim F ) ) ) |
34 |
33
|
ssrdv |
|- ( A e. ( J fLim F ) -> ( ( cls ` J ) ` { A } ) C_ ( J fLim F ) ) |