Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- U. J = U. J |
2 |
1
|
flimfil |
|- ( x e. ( J fLim F ) -> F e. ( Fil ` U. J ) ) |
3 |
2
|
ad2antlr |
|- ( ( ( S e. F /\ x e. ( J fLim F ) ) /\ y e. ( ( nei ` J ) ` { x } ) ) -> F e. ( Fil ` U. J ) ) |
4 |
|
flimnei |
|- ( ( x e. ( J fLim F ) /\ y e. ( ( nei ` J ) ` { x } ) ) -> y e. F ) |
5 |
4
|
adantll |
|- ( ( ( S e. F /\ x e. ( J fLim F ) ) /\ y e. ( ( nei ` J ) ` { x } ) ) -> y e. F ) |
6 |
|
simpll |
|- ( ( ( S e. F /\ x e. ( J fLim F ) ) /\ y e. ( ( nei ` J ) ` { x } ) ) -> S e. F ) |
7 |
|
filinn0 |
|- ( ( F e. ( Fil ` U. J ) /\ y e. F /\ S e. F ) -> ( y i^i S ) =/= (/) ) |
8 |
3 5 6 7
|
syl3anc |
|- ( ( ( S e. F /\ x e. ( J fLim F ) ) /\ y e. ( ( nei ` J ) ` { x } ) ) -> ( y i^i S ) =/= (/) ) |
9 |
8
|
ralrimiva |
|- ( ( S e. F /\ x e. ( J fLim F ) ) -> A. y e. ( ( nei ` J ) ` { x } ) ( y i^i S ) =/= (/) ) |
10 |
|
flimtop |
|- ( x e. ( J fLim F ) -> J e. Top ) |
11 |
10
|
adantl |
|- ( ( S e. F /\ x e. ( J fLim F ) ) -> J e. Top ) |
12 |
|
filelss |
|- ( ( F e. ( Fil ` U. J ) /\ S e. F ) -> S C_ U. J ) |
13 |
12
|
ancoms |
|- ( ( S e. F /\ F e. ( Fil ` U. J ) ) -> S C_ U. J ) |
14 |
2 13
|
sylan2 |
|- ( ( S e. F /\ x e. ( J fLim F ) ) -> S C_ U. J ) |
15 |
1
|
flimelbas |
|- ( x e. ( J fLim F ) -> x e. U. J ) |
16 |
15
|
adantl |
|- ( ( S e. F /\ x e. ( J fLim F ) ) -> x e. U. J ) |
17 |
1
|
neindisj2 |
|- ( ( J e. Top /\ S C_ U. J /\ x e. U. J ) -> ( x e. ( ( cls ` J ) ` S ) <-> A. y e. ( ( nei ` J ) ` { x } ) ( y i^i S ) =/= (/) ) ) |
18 |
11 14 16 17
|
syl3anc |
|- ( ( S e. F /\ x e. ( J fLim F ) ) -> ( x e. ( ( cls ` J ) ` S ) <-> A. y e. ( ( nei ` J ) ` { x } ) ( y i^i S ) =/= (/) ) ) |
19 |
9 18
|
mpbird |
|- ( ( S e. F /\ x e. ( J fLim F ) ) -> x e. ( ( cls ` J ) ` S ) ) |
20 |
19
|
ex |
|- ( S e. F -> ( x e. ( J fLim F ) -> x e. ( ( cls ` J ) ` S ) ) ) |
21 |
20
|
ssrdv |
|- ( S e. F -> ( J fLim F ) C_ ( ( cls ` J ) ` S ) ) |