Step |
Hyp |
Ref |
Expression |
1 |
|
flimcls.2 |
|- F = ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) |
2 |
|
topontop |
|- ( J e. ( TopOn ` X ) -> J e. Top ) |
3 |
2
|
3ad2ant1 |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> J e. Top ) |
4 |
|
eqid |
|- U. J = U. J |
5 |
4
|
neisspw |
|- ( J e. Top -> ( ( nei ` J ) ` { A } ) C_ ~P U. J ) |
6 |
3 5
|
syl |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( nei ` J ) ` { A } ) C_ ~P U. J ) |
7 |
|
toponuni |
|- ( J e. ( TopOn ` X ) -> X = U. J ) |
8 |
7
|
3ad2ant1 |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> X = U. J ) |
9 |
8
|
pweqd |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ~P X = ~P U. J ) |
10 |
6 9
|
sseqtrrd |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( nei ` J ) ` { A } ) C_ ~P X ) |
11 |
|
toponmax |
|- ( J e. ( TopOn ` X ) -> X e. J ) |
12 |
|
elpw2g |
|- ( X e. J -> ( S e. ~P X <-> S C_ X ) ) |
13 |
11 12
|
syl |
|- ( J e. ( TopOn ` X ) -> ( S e. ~P X <-> S C_ X ) ) |
14 |
13
|
biimpar |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X ) -> S e. ~P X ) |
15 |
14
|
3adant3 |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> S e. ~P X ) |
16 |
15
|
snssd |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> { S } C_ ~P X ) |
17 |
10 16
|
unssd |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( ( nei ` J ) ` { A } ) u. { S } ) C_ ~P X ) |
18 |
|
ssun2 |
|- { S } C_ ( ( ( nei ` J ) ` { A } ) u. { S } ) |
19 |
11
|
3ad2ant1 |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> X e. J ) |
20 |
|
simp2 |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> S C_ X ) |
21 |
19 20
|
ssexd |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> S e. _V ) |
22 |
21
|
snn0d |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> { S } =/= (/) ) |
23 |
|
ssn0 |
|- ( ( { S } C_ ( ( ( nei ` J ) ` { A } ) u. { S } ) /\ { S } =/= (/) ) -> ( ( ( nei ` J ) ` { A } ) u. { S } ) =/= (/) ) |
24 |
18 22 23
|
sylancr |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( ( nei ` J ) ` { A } ) u. { S } ) =/= (/) ) |
25 |
20 8
|
sseqtrd |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> S C_ U. J ) |
26 |
|
simp3 |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> A e. ( ( cls ` J ) ` S ) ) |
27 |
4
|
neindisj |
|- ( ( ( J e. Top /\ S C_ U. J ) /\ ( A e. ( ( cls ` J ) ` S ) /\ x e. ( ( nei ` J ) ` { A } ) ) ) -> ( x i^i S ) =/= (/) ) |
28 |
27
|
expr |
|- ( ( ( J e. Top /\ S C_ U. J ) /\ A e. ( ( cls ` J ) ` S ) ) -> ( x e. ( ( nei ` J ) ` { A } ) -> ( x i^i S ) =/= (/) ) ) |
29 |
3 25 26 28
|
syl21anc |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( x e. ( ( nei ` J ) ` { A } ) -> ( x i^i S ) =/= (/) ) ) |
30 |
29
|
imp |
|- ( ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) /\ x e. ( ( nei ` J ) ` { A } ) ) -> ( x i^i S ) =/= (/) ) |
31 |
|
elsni |
|- ( y e. { S } -> y = S ) |
32 |
31
|
ineq2d |
|- ( y e. { S } -> ( x i^i y ) = ( x i^i S ) ) |
33 |
32
|
neeq1d |
|- ( y e. { S } -> ( ( x i^i y ) =/= (/) <-> ( x i^i S ) =/= (/) ) ) |
34 |
30 33
|
syl5ibrcom |
|- ( ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) /\ x e. ( ( nei ` J ) ` { A } ) ) -> ( y e. { S } -> ( x i^i y ) =/= (/) ) ) |
35 |
34
|
ralrimiv |
|- ( ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) /\ x e. ( ( nei ` J ) ` { A } ) ) -> A. y e. { S } ( x i^i y ) =/= (/) ) |
36 |
35
|
ralrimiva |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> A. x e. ( ( nei ` J ) ` { A } ) A. y e. { S } ( x i^i y ) =/= (/) ) |
37 |
|
simp1 |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> J e. ( TopOn ` X ) ) |
38 |
4
|
clsss3 |
|- ( ( J e. Top /\ S C_ U. J ) -> ( ( cls ` J ) ` S ) C_ U. J ) |
39 |
3 25 38
|
syl2anc |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( cls ` J ) ` S ) C_ U. J ) |
40 |
39 26
|
sseldd |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> A e. U. J ) |
41 |
40 8
|
eleqtrrd |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> A e. X ) |
42 |
41
|
snssd |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> { A } C_ X ) |
43 |
|
snnzg |
|- ( A e. ( ( cls ` J ) ` S ) -> { A } =/= (/) ) |
44 |
43
|
3ad2ant3 |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> { A } =/= (/) ) |
45 |
|
neifil |
|- ( ( J e. ( TopOn ` X ) /\ { A } C_ X /\ { A } =/= (/) ) -> ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) ) |
46 |
37 42 44 45
|
syl3anc |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) ) |
47 |
|
filfbas |
|- ( ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) -> ( ( nei ` J ) ` { A } ) e. ( fBas ` X ) ) |
48 |
46 47
|
syl |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( nei ` J ) ` { A } ) e. ( fBas ` X ) ) |
49 |
|
ne0i |
|- ( A e. ( ( cls ` J ) ` S ) -> ( ( cls ` J ) ` S ) =/= (/) ) |
50 |
49
|
3ad2ant3 |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( cls ` J ) ` S ) =/= (/) ) |
51 |
|
cls0 |
|- ( J e. Top -> ( ( cls ` J ) ` (/) ) = (/) ) |
52 |
3 51
|
syl |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( cls ` J ) ` (/) ) = (/) ) |
53 |
50 52
|
neeqtrrd |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( cls ` J ) ` S ) =/= ( ( cls ` J ) ` (/) ) ) |
54 |
|
fveq2 |
|- ( S = (/) -> ( ( cls ` J ) ` S ) = ( ( cls ` J ) ` (/) ) ) |
55 |
54
|
necon3i |
|- ( ( ( cls ` J ) ` S ) =/= ( ( cls ` J ) ` (/) ) -> S =/= (/) ) |
56 |
53 55
|
syl |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> S =/= (/) ) |
57 |
|
snfbas |
|- ( ( S C_ X /\ S =/= (/) /\ X e. J ) -> { S } e. ( fBas ` X ) ) |
58 |
20 56 19 57
|
syl3anc |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> { S } e. ( fBas ` X ) ) |
59 |
|
fbunfip |
|- ( ( ( ( nei ` J ) ` { A } ) e. ( fBas ` X ) /\ { S } e. ( fBas ` X ) ) -> ( -. (/) e. ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) <-> A. x e. ( ( nei ` J ) ` { A } ) A. y e. { S } ( x i^i y ) =/= (/) ) ) |
60 |
48 58 59
|
syl2anc |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( -. (/) e. ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) <-> A. x e. ( ( nei ` J ) ` { A } ) A. y e. { S } ( x i^i y ) =/= (/) ) ) |
61 |
36 60
|
mpbird |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> -. (/) e. ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) |
62 |
|
fsubbas |
|- ( X e. J -> ( ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) e. ( fBas ` X ) <-> ( ( ( ( nei ` J ) ` { A } ) u. { S } ) C_ ~P X /\ ( ( ( nei ` J ) ` { A } ) u. { S } ) =/= (/) /\ -. (/) e. ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) ) ) |
63 |
19 62
|
syl |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) e. ( fBas ` X ) <-> ( ( ( ( nei ` J ) ` { A } ) u. { S } ) C_ ~P X /\ ( ( ( nei ` J ) ` { A } ) u. { S } ) =/= (/) /\ -. (/) e. ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) ) ) |
64 |
17 24 61 63
|
mpbir3and |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) e. ( fBas ` X ) ) |
65 |
|
fgcl |
|- ( ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) e. ( fBas ` X ) -> ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) e. ( Fil ` X ) ) |
66 |
64 65
|
syl |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) e. ( Fil ` X ) ) |
67 |
1 66
|
eqeltrid |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> F e. ( Fil ` X ) ) |
68 |
|
fvex |
|- ( ( nei ` J ) ` { A } ) e. _V |
69 |
|
snex |
|- { S } e. _V |
70 |
68 69
|
unex |
|- ( ( ( nei ` J ) ` { A } ) u. { S } ) e. _V |
71 |
|
ssfii |
|- ( ( ( ( nei ` J ) ` { A } ) u. { S } ) e. _V -> ( ( ( nei ` J ) ` { A } ) u. { S } ) C_ ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) |
72 |
70 71
|
ax-mp |
|- ( ( ( nei ` J ) ` { A } ) u. { S } ) C_ ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) |
73 |
|
ssfg |
|- ( ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) e. ( fBas ` X ) -> ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) C_ ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) ) |
74 |
64 73
|
syl |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) C_ ( X filGen ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) ) |
75 |
74 1
|
sseqtrrdi |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( fi ` ( ( ( nei ` J ) ` { A } ) u. { S } ) ) C_ F ) |
76 |
72 75
|
sstrid |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( ( nei ` J ) ` { A } ) u. { S } ) C_ F ) |
77 |
|
snssg |
|- ( S e. _V -> ( S e. ( ( ( nei ` J ) ` { A } ) u. { S } ) <-> { S } C_ ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) |
78 |
21 77
|
syl |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( S e. ( ( ( nei ` J ) ` { A } ) u. { S } ) <-> { S } C_ ( ( ( nei ` J ) ` { A } ) u. { S } ) ) ) |
79 |
18 78
|
mpbiri |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> S e. ( ( ( nei ` J ) ` { A } ) u. { S } ) ) |
80 |
76 79
|
sseldd |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> S e. F ) |
81 |
76
|
unssad |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( ( nei ` J ) ` { A } ) C_ F ) |
82 |
|
elflim |
|- ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) ) |
83 |
37 67 82
|
syl2anc |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) ) |
84 |
41 81 83
|
mpbir2and |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> A e. ( J fLim F ) ) |
85 |
67 80 84
|
3jca |
|- ( ( J e. ( TopOn ` X ) /\ S C_ X /\ A e. ( ( cls ` J ) ` S ) ) -> ( F e. ( Fil ` X ) /\ S e. F /\ A e. ( J fLim F ) ) ) |