Step |
Hyp |
Ref |
Expression |
1 |
|
simp2 |
|- ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) -> A e. ( J fClus L ) ) |
2 |
|
eqid |
|- U. J = U. J |
3 |
2
|
fclsfil |
|- ( A e. ( J fClus L ) -> L e. ( Fil ` U. J ) ) |
4 |
3
|
3ad2ant2 |
|- ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) -> L e. ( Fil ` U. J ) ) |
5 |
|
fclsfnflim |
|- ( L e. ( Fil ` U. J ) -> ( A e. ( J fClus L ) <-> E. f e. ( Fil ` U. J ) ( L C_ f /\ A e. ( J fLim f ) ) ) ) |
6 |
4 5
|
syl |
|- ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) -> ( A e. ( J fClus L ) <-> E. f e. ( Fil ` U. J ) ( L C_ f /\ A e. ( J fLim f ) ) ) ) |
7 |
1 6
|
mpbid |
|- ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) -> E. f e. ( Fil ` U. J ) ( L C_ f /\ A e. ( J fLim f ) ) ) |
8 |
|
simpl1 |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> K e. Top ) |
9 |
|
toptopon2 |
|- ( K e. Top <-> K e. ( TopOn ` U. K ) ) |
10 |
8 9
|
sylib |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> K e. ( TopOn ` U. K ) ) |
11 |
|
simprl |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> f e. ( Fil ` U. J ) ) |
12 |
|
eqid |
|- U. K = U. K |
13 |
2 12
|
cnpf |
|- ( F e. ( ( J CnP K ) ` A ) -> F : U. J --> U. K ) |
14 |
13
|
3ad2ant3 |
|- ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) -> F : U. J --> U. K ) |
15 |
14
|
adantr |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> F : U. J --> U. K ) |
16 |
|
flfssfcf |
|- ( ( K e. ( TopOn ` U. K ) /\ f e. ( Fil ` U. J ) /\ F : U. J --> U. K ) -> ( ( K fLimf f ) ` F ) C_ ( ( K fClusf f ) ` F ) ) |
17 |
10 11 15 16
|
syl3anc |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> ( ( K fLimf f ) ` F ) C_ ( ( K fClusf f ) ` F ) ) |
18 |
12
|
topopn |
|- ( K e. Top -> U. K e. K ) |
19 |
8 18
|
syl |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> U. K e. K ) |
20 |
4
|
adantr |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> L e. ( Fil ` U. J ) ) |
21 |
|
filfbas |
|- ( L e. ( Fil ` U. J ) -> L e. ( fBas ` U. J ) ) |
22 |
20 21
|
syl |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> L e. ( fBas ` U. J ) ) |
23 |
|
fmfil |
|- ( ( U. K e. K /\ L e. ( fBas ` U. J ) /\ F : U. J --> U. K ) -> ( ( U. K FilMap F ) ` L ) e. ( Fil ` U. K ) ) |
24 |
19 22 15 23
|
syl3anc |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> ( ( U. K FilMap F ) ` L ) e. ( Fil ` U. K ) ) |
25 |
|
filfbas |
|- ( f e. ( Fil ` U. J ) -> f e. ( fBas ` U. J ) ) |
26 |
25
|
ad2antrl |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> f e. ( fBas ` U. J ) ) |
27 |
|
simprrl |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> L C_ f ) |
28 |
|
fmss |
|- ( ( ( U. K e. K /\ L e. ( fBas ` U. J ) /\ f e. ( fBas ` U. J ) ) /\ ( F : U. J --> U. K /\ L C_ f ) ) -> ( ( U. K FilMap F ) ` L ) C_ ( ( U. K FilMap F ) ` f ) ) |
29 |
19 22 26 15 27 28
|
syl32anc |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> ( ( U. K FilMap F ) ` L ) C_ ( ( U. K FilMap F ) ` f ) ) |
30 |
|
fclsss2 |
|- ( ( K e. ( TopOn ` U. K ) /\ ( ( U. K FilMap F ) ` L ) e. ( Fil ` U. K ) /\ ( ( U. K FilMap F ) ` L ) C_ ( ( U. K FilMap F ) ` f ) ) -> ( K fClus ( ( U. K FilMap F ) ` f ) ) C_ ( K fClus ( ( U. K FilMap F ) ` L ) ) ) |
31 |
10 24 29 30
|
syl3anc |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> ( K fClus ( ( U. K FilMap F ) ` f ) ) C_ ( K fClus ( ( U. K FilMap F ) ` L ) ) ) |
32 |
|
fcfval |
|- ( ( K e. ( TopOn ` U. K ) /\ f e. ( Fil ` U. J ) /\ F : U. J --> U. K ) -> ( ( K fClusf f ) ` F ) = ( K fClus ( ( U. K FilMap F ) ` f ) ) ) |
33 |
10 11 15 32
|
syl3anc |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> ( ( K fClusf f ) ` F ) = ( K fClus ( ( U. K FilMap F ) ` f ) ) ) |
34 |
|
fcfval |
|- ( ( K e. ( TopOn ` U. K ) /\ L e. ( Fil ` U. J ) /\ F : U. J --> U. K ) -> ( ( K fClusf L ) ` F ) = ( K fClus ( ( U. K FilMap F ) ` L ) ) ) |
35 |
10 20 15 34
|
syl3anc |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> ( ( K fClusf L ) ` F ) = ( K fClus ( ( U. K FilMap F ) ` L ) ) ) |
36 |
31 33 35
|
3sstr4d |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> ( ( K fClusf f ) ` F ) C_ ( ( K fClusf L ) ` F ) ) |
37 |
17 36
|
sstrd |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> ( ( K fLimf f ) ` F ) C_ ( ( K fClusf L ) ` F ) ) |
38 |
|
simprrr |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> A e. ( J fLim f ) ) |
39 |
|
simpl3 |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> F e. ( ( J CnP K ) ` A ) ) |
40 |
|
cnpflfi |
|- ( ( A e. ( J fLim f ) /\ F e. ( ( J CnP K ) ` A ) ) -> ( F ` A ) e. ( ( K fLimf f ) ` F ) ) |
41 |
38 39 40
|
syl2anc |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> ( F ` A ) e. ( ( K fLimf f ) ` F ) ) |
42 |
37 41
|
sseldd |
|- ( ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) /\ ( f e. ( Fil ` U. J ) /\ ( L C_ f /\ A e. ( J fLim f ) ) ) ) -> ( F ` A ) e. ( ( K fClusf L ) ` F ) ) |
43 |
7 42
|
rexlimddv |
|- ( ( K e. Top /\ A e. ( J fClus L ) /\ F e. ( ( J CnP K ) ` A ) ) -> ( F ` A ) e. ( ( K fClusf L ) ` F ) ) |