Metamath Proof Explorer

Theorem fclscmpi

Description: Forward direction of fclscmp . Every filter clusters in a compact space. (Contributed by Mario Carneiro, 11-Apr-2015) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Hypothesis flimfnfcls.x 
|- X = U. J
Assertion fclscmpi 
|- ( ( J e. Comp /\ F e. ( Fil ` X ) ) -> ( J fClus F ) =/= (/) )

Proof

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 ) =/= (/) )