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 ⊢ 𝑋 = ∪ 𝐽
Assertion fclscmpi ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐽 fClus 𝐹 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 flimfnfcls.x ⊢ 𝑋 = ∪ 𝐽
2 cmptop ⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top )
3 1 fclsval ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐽 fClus 𝐹 ) = if ( 𝑋 = 𝑋 , ∩ 𝑥 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) , ∅ ) )
4 eqid ⊢ 𝑋 = 𝑋
5 4 iftruei ⊢ if ( 𝑋 = 𝑋 , ∩ 𝑥 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) , ∅ ) = ∩ 𝑥 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑥 )
6 3 5 eqtrdi ⊢ ( ( 𝐽 ∈ Top ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐽 fClus 𝐹 ) = ∩ 𝑥 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) )
7 2 6 sylan ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐽 fClus 𝐹 ) = ∩ 𝑥 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) )
8 fvex ⊢ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∈ V
9 8 dfiin3 ⊢ ∩ 𝑥 ∈ 𝐹 ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) = ∩ ran ( 𝑥 ∈ 𝐹 ↦ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) )
10 7 9 eqtrdi ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐽 fClus 𝐹 ) = ∩ ran ( 𝑥 ∈ 𝐹 ↦ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) )
11 simpl ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → 𝐽 ∈ Comp )
12 11 adantr ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐹 ) → 𝐽 ∈ Comp )
13 12 2 syl ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐹 ) → 𝐽 ∈ Top )
14 filelss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ⊆ 𝑋 )
15 14 adantll ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ⊆ 𝑋 )
16 1 clscld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) )
17 13 15 16 syl2anc ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐹 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) )
18 17 fmpttd ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑥 ∈ 𝐹 ↦ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) : 𝐹 ⟶ ( Clsd ‘ 𝐽 ) )
19 18 frnd ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ran ( 𝑥 ∈ 𝐹 ↦ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ⊆ ( Clsd ‘ 𝐽 ) )
20 simpr ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
21 20 adantr ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐹 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
22 simpr ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ∈ 𝐹 )
23 1 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑋 )
24 13 15 23 syl2anc ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐹 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑋 )
25 1 sscls ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ 𝑋 ) → 𝑥 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) )
26 13 15 25 syl2anc ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) )
27 filss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝐹 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑋 ∧ 𝑥 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∈ 𝐹 )
28 21 22 24 26 27 syl13anc ⊢ ( ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐹 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∈ 𝐹 )
29 28 fmpttd ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑥 ∈ 𝐹 ↦ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) : 𝐹 ⟶ 𝐹 )
30 29 frnd ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ran ( 𝑥 ∈ 𝐹 ↦ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ⊆ 𝐹 )
31 fiss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ran ( 𝑥 ∈ 𝐹 ↦ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ⊆ 𝐹 ) → ( fi ‘ ran ( 𝑥 ∈ 𝐹 ↦ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) ⊆ ( fi ‘ 𝐹 ) )
32 20 30 31 syl2anc ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( fi ‘ ran ( 𝑥 ∈ 𝐹 ↦ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) ⊆ ( fi ‘ 𝐹 ) )
33 filfi ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( fi ‘ 𝐹 ) = 𝐹 )
34 20 33 syl ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( fi ‘ 𝐹 ) = 𝐹 )
35 32 34 sseqtrd ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( fi ‘ ran ( 𝑥 ∈ 𝐹 ↦ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) ⊆ 𝐹 )
36 0nelfil ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ¬ ∅ ∈ 𝐹 )
37 20 36 syl ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ¬ ∅ ∈ 𝐹 )
38 35 37 ssneldd ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ¬ ∅ ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐹 ↦ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) )
39 cmpfii ⊢ ( ( 𝐽 ∈ Comp ∧ ran ( 𝑥 ∈ 𝐹 ↦ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ⊆ ( Clsd ‘ 𝐽 ) ∧ ¬ ∅ ∈ ( fi ‘ ran ( 𝑥 ∈ 𝐹 ↦ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) ) → ∩ ran ( 𝑥 ∈ 𝐹 ↦ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ≠ ∅ )
40 11 19 38 39 syl3anc ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ∩ ran ( 𝑥 ∈ 𝐹 ↦ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ≠ ∅ )
41 10 40 eqnetrd ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐽 fClus 𝐹 ) ≠ ∅ )