Step |
Hyp |
Ref |
Expression |
1 |
|
flimfnfcls.x |
|- X = U. J |
2 |
|
cmptop |
|- ( J e. Comp -> J e. Top ) |
3 |
1
|
fclsval |
|- ( ( J e. Top /\ F e. ( Fil ` X ) ) -> ( J fClus F ) = if ( X = X , |^|_ x e. F ( ( cls ` J ) ` x ) , (/) ) ) |
4 |
|
eqid |
|- X = X |
5 |
4
|
iftruei |
|- if ( X = X , |^|_ x e. F ( ( cls ` J ) ` x ) , (/) ) = |^|_ x e. F ( ( cls ` J ) ` x ) |
6 |
3 5
|
eqtrdi |
|- ( ( J e. Top /\ F e. ( Fil ` X ) ) -> ( J fClus F ) = |^|_ x e. F ( ( cls ` J ) ` x ) ) |
7 |
2 6
|
sylan |
|- ( ( J e. Comp /\ F e. ( Fil ` X ) ) -> ( J fClus F ) = |^|_ x e. F ( ( cls ` J ) ` x ) ) |
8 |
|
fvex |
|- ( ( cls ` J ) ` x ) e. _V |
9 |
8
|
dfiin3 |
|- |^|_ x e. F ( ( cls ` J ) ` x ) = |^| ran ( x e. F |-> ( ( cls ` J ) ` x ) ) |
10 |
7 9
|
eqtrdi |
|- ( ( J e. Comp /\ F e. ( Fil ` X ) ) -> ( J fClus F ) = |^| ran ( x e. F |-> ( ( cls ` J ) ` x ) ) ) |
11 |
|
simpl |
|- ( ( J e. Comp /\ F e. ( Fil ` X ) ) -> J e. Comp ) |
12 |
11
|
adantr |
|- ( ( ( J e. Comp /\ F e. ( Fil ` X ) ) /\ x e. F ) -> J e. Comp ) |
13 |
12 2
|
syl |
|- ( ( ( J e. Comp /\ F e. ( Fil ` X ) ) /\ x e. F ) -> J e. Top ) |
14 |
|
filelss |
|- ( ( F e. ( Fil ` X ) /\ x e. F ) -> x C_ X ) |
15 |
14
|
adantll |
|- ( ( ( J e. Comp /\ F e. ( Fil ` X ) ) /\ x e. F ) -> x C_ X ) |
16 |
1
|
clscld |
|- ( ( J e. Top /\ x C_ X ) -> ( ( cls ` J ) ` x ) e. ( Clsd ` J ) ) |
17 |
13 15 16
|
syl2anc |
|- ( ( ( J e. Comp /\ F e. ( Fil ` X ) ) /\ x e. F ) -> ( ( cls ` J ) ` x ) e. ( Clsd ` J ) ) |
18 |
17
|
fmpttd |
|- ( ( J e. Comp /\ F e. ( Fil ` X ) ) -> ( x e. F |-> ( ( cls ` J ) ` x ) ) : F --> ( Clsd ` J ) ) |
19 |
18
|
frnd |
|- ( ( J e. Comp /\ F e. ( Fil ` X ) ) -> ran ( x e. F |-> ( ( cls ` J ) ` x ) ) C_ ( Clsd ` J ) ) |
20 |
|
simpr |
|- ( ( J e. Comp /\ F e. ( Fil ` X ) ) -> F e. ( Fil ` X ) ) |
21 |
20
|
adantr |
|- ( ( ( J e. Comp /\ F e. ( Fil ` X ) ) /\ x e. F ) -> F e. ( Fil ` X ) ) |
22 |
|
simpr |
|- ( ( ( J e. Comp /\ F e. ( Fil ` X ) ) /\ x e. F ) -> x e. F ) |
23 |
1
|
clsss3 |
|- ( ( J e. Top /\ x C_ X ) -> ( ( cls ` J ) ` x ) C_ X ) |
24 |
13 15 23
|
syl2anc |
|- ( ( ( J e. Comp /\ F e. ( Fil ` X ) ) /\ x e. F ) -> ( ( cls ` J ) ` x ) C_ X ) |
25 |
1
|
sscls |
|- ( ( J e. Top /\ x C_ X ) -> x C_ ( ( cls ` J ) ` x ) ) |
26 |
13 15 25
|
syl2anc |
|- ( ( ( J e. Comp /\ F e. ( Fil ` X ) ) /\ x e. F ) -> x C_ ( ( cls ` J ) ` x ) ) |
27 |
|
filss |
|- ( ( F e. ( Fil ` X ) /\ ( x e. F /\ ( ( cls ` J ) ` x ) C_ X /\ x C_ ( ( cls ` J ) ` x ) ) ) -> ( ( cls ` J ) ` x ) e. F ) |
28 |
21 22 24 26 27
|
syl13anc |
|- ( ( ( J e. Comp /\ F e. ( Fil ` X ) ) /\ x e. F ) -> ( ( cls ` J ) ` x ) e. F ) |
29 |
28
|
fmpttd |
|- ( ( J e. Comp /\ F e. ( Fil ` X ) ) -> ( x e. F |-> ( ( cls ` J ) ` x ) ) : F --> F ) |
30 |
29
|
frnd |
|- ( ( J e. Comp /\ F e. ( Fil ` X ) ) -> ran ( x e. F |-> ( ( cls ` J ) ` x ) ) C_ F ) |
31 |
|
fiss |
|- ( ( F e. ( Fil ` X ) /\ ran ( x e. F |-> ( ( cls ` J ) ` x ) ) C_ F ) -> ( fi ` ran ( x e. F |-> ( ( cls ` J ) ` x ) ) ) C_ ( fi ` F ) ) |
32 |
20 30 31
|
syl2anc |
|- ( ( J e. Comp /\ F e. ( Fil ` X ) ) -> ( fi ` ran ( x e. F |-> ( ( cls ` J ) ` x ) ) ) C_ ( fi ` F ) ) |
33 |
|
filfi |
|- ( F e. ( Fil ` X ) -> ( fi ` F ) = F ) |
34 |
20 33
|
syl |
|- ( ( J e. Comp /\ F e. ( Fil ` X ) ) -> ( fi ` F ) = F ) |
35 |
32 34
|
sseqtrd |
|- ( ( J e. Comp /\ F e. ( Fil ` X ) ) -> ( fi ` ran ( x e. F |-> ( ( cls ` J ) ` x ) ) ) C_ F ) |
36 |
|
0nelfil |
|- ( F e. ( Fil ` X ) -> -. (/) e. F ) |
37 |
20 36
|
syl |
|- ( ( J e. Comp /\ F e. ( Fil ` X ) ) -> -. (/) e. F ) |
38 |
35 37
|
ssneldd |
|- ( ( J e. Comp /\ F e. ( Fil ` X ) ) -> -. (/) e. ( fi ` ran ( x e. F |-> ( ( cls ` J ) ` x ) ) ) ) |
39 |
|
cmpfii |
|- ( ( J e. Comp /\ ran ( x e. F |-> ( ( cls ` J ) ` x ) ) C_ ( Clsd ` J ) /\ -. (/) e. ( fi ` ran ( x e. F |-> ( ( cls ` J ) ` x ) ) ) ) -> |^| ran ( x e. F |-> ( ( cls ` J ) ` x ) ) =/= (/) ) |
40 |
11 19 38 39
|
syl3anc |
|- ( ( J e. Comp /\ F e. ( Fil ` X ) ) -> |^| ran ( x e. F |-> ( ( cls ` J ) ` x ) ) =/= (/) ) |
41 |
10 40
|
eqnetrd |
|- ( ( J e. Comp /\ F e. ( Fil ` X ) ) -> ( J fClus F ) =/= (/) ) |