Step |
Hyp |
Ref |
Expression |
1 |
|
filsspw |
|- ( F e. ( Fil ` X ) -> F C_ ~P X ) |
2 |
1
|
adantr |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> F C_ ~P X ) |
3 |
|
fclstop |
|- ( A e. ( J fClus F ) -> J e. Top ) |
4 |
3
|
adantl |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> J e. Top ) |
5 |
|
eqid |
|- U. J = U. J |
6 |
5
|
neisspw |
|- ( J e. Top -> ( ( nei ` J ) ` { A } ) C_ ~P U. J ) |
7 |
4 6
|
syl |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( nei ` J ) ` { A } ) C_ ~P U. J ) |
8 |
|
filunibas |
|- ( F e. ( Fil ` X ) -> U. F = X ) |
9 |
5
|
fclsfil |
|- ( A e. ( J fClus F ) -> F e. ( Fil ` U. J ) ) |
10 |
|
filunibas |
|- ( F e. ( Fil ` U. J ) -> U. F = U. J ) |
11 |
9 10
|
syl |
|- ( A e. ( J fClus F ) -> U. F = U. J ) |
12 |
8 11
|
sylan9req |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> X = U. J ) |
13 |
12
|
pweqd |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ~P X = ~P U. J ) |
14 |
7 13
|
sseqtrrd |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( nei ` J ) ` { A } ) C_ ~P X ) |
15 |
2 14
|
unssd |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( F u. ( ( nei ` J ) ` { A } ) ) C_ ~P X ) |
16 |
|
ssun1 |
|- F C_ ( F u. ( ( nei ` J ) ` { A } ) ) |
17 |
|
filn0 |
|- ( F e. ( Fil ` X ) -> F =/= (/) ) |
18 |
|
ssn0 |
|- ( ( F C_ ( F u. ( ( nei ` J ) ` { A } ) ) /\ F =/= (/) ) -> ( F u. ( ( nei ` J ) ` { A } ) ) =/= (/) ) |
19 |
16 17 18
|
sylancr |
|- ( F e. ( Fil ` X ) -> ( F u. ( ( nei ` J ) ` { A } ) ) =/= (/) ) |
20 |
19
|
adantr |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( F u. ( ( nei ` J ) ` { A } ) ) =/= (/) ) |
21 |
|
incom |
|- ( y i^i x ) = ( x i^i y ) |
22 |
|
fclsneii |
|- ( ( A e. ( J fClus F ) /\ y e. ( ( nei ` J ) ` { A } ) /\ x e. F ) -> ( y i^i x ) =/= (/) ) |
23 |
21 22
|
eqnetrrid |
|- ( ( A e. ( J fClus F ) /\ y e. ( ( nei ` J ) ` { A } ) /\ x e. F ) -> ( x i^i y ) =/= (/) ) |
24 |
23
|
3com23 |
|- ( ( A e. ( J fClus F ) /\ x e. F /\ y e. ( ( nei ` J ) ` { A } ) ) -> ( x i^i y ) =/= (/) ) |
25 |
24
|
3expb |
|- ( ( A e. ( J fClus F ) /\ ( x e. F /\ y e. ( ( nei ` J ) ` { A } ) ) ) -> ( x i^i y ) =/= (/) ) |
26 |
25
|
adantll |
|- ( ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) /\ ( x e. F /\ y e. ( ( nei ` J ) ` { A } ) ) ) -> ( x i^i y ) =/= (/) ) |
27 |
26
|
ralrimivva |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> A. x e. F A. y e. ( ( nei ` J ) ` { A } ) ( x i^i y ) =/= (/) ) |
28 |
|
filfbas |
|- ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) ) |
29 |
28
|
adantr |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> F e. ( fBas ` X ) ) |
30 |
|
istopon |
|- ( J e. ( TopOn ` X ) <-> ( J e. Top /\ X = U. J ) ) |
31 |
4 12 30
|
sylanbrc |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> J e. ( TopOn ` X ) ) |
32 |
5
|
fclselbas |
|- ( A e. ( J fClus F ) -> A e. U. J ) |
33 |
32
|
adantl |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> A e. U. J ) |
34 |
33 12
|
eleqtrrd |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> A e. X ) |
35 |
34
|
snssd |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> { A } C_ X ) |
36 |
|
snnzg |
|- ( A e. ( J fClus F ) -> { A } =/= (/) ) |
37 |
36
|
adantl |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> { A } =/= (/) ) |
38 |
|
neifil |
|- ( ( J e. ( TopOn ` X ) /\ { A } C_ X /\ { A } =/= (/) ) -> ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) ) |
39 |
31 35 37 38
|
syl3anc |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) ) |
40 |
|
filfbas |
|- ( ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) -> ( ( nei ` J ) ` { A } ) e. ( fBas ` X ) ) |
41 |
39 40
|
syl |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( nei ` J ) ` { A } ) e. ( fBas ` X ) ) |
42 |
|
fbunfip |
|- ( ( F e. ( fBas ` X ) /\ ( ( nei ` J ) ` { A } ) e. ( fBas ` X ) ) -> ( -. (/) e. ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) <-> A. x e. F A. y e. ( ( nei ` J ) ` { A } ) ( x i^i y ) =/= (/) ) ) |
43 |
29 41 42
|
syl2anc |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( -. (/) e. ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) <-> A. x e. F A. y e. ( ( nei ` J ) ` { A } ) ( x i^i y ) =/= (/) ) ) |
44 |
27 43
|
mpbird |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> -. (/) e. ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) |
45 |
|
filtop |
|- ( F e. ( Fil ` X ) -> X e. F ) |
46 |
|
fsubbas |
|- ( X e. F -> ( ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) e. ( fBas ` X ) <-> ( ( F u. ( ( nei ` J ) ` { A } ) ) C_ ~P X /\ ( F u. ( ( nei ` J ) ` { A } ) ) =/= (/) /\ -. (/) e. ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) |
47 |
45 46
|
syl |
|- ( F e. ( Fil ` X ) -> ( ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) e. ( fBas ` X ) <-> ( ( F u. ( ( nei ` J ) ` { A } ) ) C_ ~P X /\ ( F u. ( ( nei ` J ) ` { A } ) ) =/= (/) /\ -. (/) e. ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) |
48 |
47
|
adantr |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) e. ( fBas ` X ) <-> ( ( F u. ( ( nei ` J ) ` { A } ) ) C_ ~P X /\ ( F u. ( ( nei ` J ) ` { A } ) ) =/= (/) /\ -. (/) e. ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) |
49 |
15 20 44 48
|
mpbir3and |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) e. ( fBas ` X ) ) |
50 |
|
fgcl |
|- ( ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) e. ( fBas ` X ) -> ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) e. ( Fil ` X ) ) |
51 |
49 50
|
syl |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) e. ( Fil ` X ) ) |
52 |
|
fvex |
|- ( ( nei ` J ) ` { A } ) e. _V |
53 |
|
unexg |
|- ( ( F e. ( Fil ` X ) /\ ( ( nei ` J ) ` { A } ) e. _V ) -> ( F u. ( ( nei ` J ) ` { A } ) ) e. _V ) |
54 |
52 53
|
mpan2 |
|- ( F e. ( Fil ` X ) -> ( F u. ( ( nei ` J ) ` { A } ) ) e. _V ) |
55 |
|
ssfii |
|- ( ( F u. ( ( nei ` J ) ` { A } ) ) e. _V -> ( F u. ( ( nei ` J ) ` { A } ) ) C_ ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) |
56 |
54 55
|
syl |
|- ( F e. ( Fil ` X ) -> ( F u. ( ( nei ` J ) ` { A } ) ) C_ ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) |
57 |
56
|
adantr |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( F u. ( ( nei ` J ) ` { A } ) ) C_ ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) |
58 |
57
|
unssad |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> F C_ ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) |
59 |
|
ssfg |
|- ( ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) e. ( fBas ` X ) -> ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) |
60 |
49 59
|
syl |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) |
61 |
58 60
|
sstrd |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> F C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) |
62 |
57
|
unssbd |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( nei ` J ) ` { A } ) C_ ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) |
63 |
62 60
|
sstrd |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( nei ` J ) ` { A } ) C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) |
64 |
|
elflim |
|- ( ( J e. ( TopOn ` X ) /\ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) e. ( Fil ` X ) ) -> ( A e. ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) ) |
65 |
31 51 64
|
syl2anc |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( A e. ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) ) |
66 |
34 63 65
|
mpbir2and |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> A e. ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) |
67 |
|
sseq2 |
|- ( g = ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) -> ( F C_ g <-> F C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) |
68 |
|
oveq2 |
|- ( g = ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) -> ( J fLim g ) = ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) |
69 |
68
|
eleq2d |
|- ( g = ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) -> ( A e. ( J fLim g ) <-> A e. ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) ) |
70 |
67 69
|
anbi12d |
|- ( g = ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) -> ( ( F C_ g /\ A e. ( J fLim g ) ) <-> ( F C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) /\ A e. ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) ) ) |
71 |
70
|
rspcev |
|- ( ( ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) e. ( Fil ` X ) /\ ( F C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) /\ A e. ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) ) -> E. g e. ( Fil ` X ) ( F C_ g /\ A e. ( J fLim g ) ) ) |
72 |
51 61 66 71
|
syl12anc |
|- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> E. g e. ( Fil ` X ) ( F C_ g /\ A e. ( J fLim g ) ) ) |
73 |
72
|
ex |
|- ( F e. ( Fil ` X ) -> ( A e. ( J fClus F ) -> E. g e. ( Fil ` X ) ( F C_ g /\ A e. ( J fLim g ) ) ) ) |
74 |
|
simprl |
|- ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> g e. ( Fil ` X ) ) |
75 |
|
simprrr |
|- ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> A e. ( J fLim g ) ) |
76 |
|
flimtopon |
|- ( A e. ( J fLim g ) -> ( J e. ( TopOn ` X ) <-> g e. ( Fil ` X ) ) ) |
77 |
75 76
|
syl |
|- ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> ( J e. ( TopOn ` X ) <-> g e. ( Fil ` X ) ) ) |
78 |
74 77
|
mpbird |
|- ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> J e. ( TopOn ` X ) ) |
79 |
|
simpl |
|- ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> F e. ( Fil ` X ) ) |
80 |
|
simprrl |
|- ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> F C_ g ) |
81 |
|
fclsss2 |
|- ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) /\ F C_ g ) -> ( J fClus g ) C_ ( J fClus F ) ) |
82 |
78 79 80 81
|
syl3anc |
|- ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> ( J fClus g ) C_ ( J fClus F ) ) |
83 |
|
flimfcls |
|- ( J fLim g ) C_ ( J fClus g ) |
84 |
83 75
|
sselid |
|- ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> A e. ( J fClus g ) ) |
85 |
82 84
|
sseldd |
|- ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> A e. ( J fClus F ) ) |
86 |
85
|
rexlimdvaa |
|- ( F e. ( Fil ` X ) -> ( E. g e. ( Fil ` X ) ( F C_ g /\ A e. ( J fLim g ) ) -> A e. ( J fClus F ) ) ) |
87 |
73 86
|
impbid |
|- ( F e. ( Fil ` X ) -> ( A e. ( J fClus F ) <-> E. g e. ( Fil ` X ) ( F C_ g /\ A e. ( J fLim g ) ) ) ) |