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