This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ufilcmp

Description: A space is compact iff every ultrafilter converges. (Contributed by Jeff Hankins, 11-Dec-2009) (Proof shortened by Mario Carneiro, 12-Apr-2015) (Revised by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion ufilcmp ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝐽 ∈ Comp ↔ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 ufilfil ⊢ ( 𝑓 ∈ ( UFil ‘ ∪ 𝐽 ) → 𝑓 ∈ ( Fil ‘ ∪ 𝐽 ) )
2 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
3 2 fclscmpi ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑓 ∈ ( Fil ‘ ∪ 𝐽 ) ) → ( 𝐽 fClus 𝑓 ) ≠ ∅ )
4 1 3 sylan2 ⊢ ( ( 𝐽 ∈ Comp ∧ 𝑓 ∈ ( UFil ‘ ∪ 𝐽 ) ) → ( 𝐽 fClus 𝑓 ) ≠ ∅ )
5 4 ralrimiva ⊢ ( 𝐽 ∈ Comp → ∀ 𝑓 ∈ ( UFil ‘ ∪ 𝐽 ) ( 𝐽 fClus 𝑓 ) ≠ ∅ )
6 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
7 6 fveq2d ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( UFil ‘ 𝑋 ) = ( UFil ‘ ∪ 𝐽 ) )
8 7 raleqdv ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fClus 𝑓 ) ≠ ∅ ↔ ∀ 𝑓 ∈ ( UFil ‘ ∪ 𝐽 ) ( 𝐽 fClus 𝑓 ) ≠ ∅ ) )
9 8 adantl ⊢ ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fClus 𝑓 ) ≠ ∅ ↔ ∀ 𝑓 ∈ ( UFil ‘ ∪ 𝐽 ) ( 𝐽 fClus 𝑓 ) ≠ ∅ ) )
10 5 9 imbitrrid ⊢ ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝐽 ∈ Comp → ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fClus 𝑓 ) ≠ ∅ ) )
11 ufli ⊢ ( ( 𝑋 ∈ UFL ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝑔 ⊆ 𝑓 )
12 11 adantlr ⊢ ( ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝑔 ⊆ 𝑓 )
13 r19.29 ⊢ ( ( ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fClus 𝑓 ) ≠ ∅ ∧ ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝑔 ⊆ 𝑓 ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( ( 𝐽 fClus 𝑓 ) ≠ ∅ ∧ 𝑔 ⊆ 𝑓 ) )
14 simpllr ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑔 ⊆ 𝑓 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
15 simplr ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑔 ⊆ 𝑓 ) ) → 𝑔 ∈ ( Fil ‘ 𝑋 ) )
16 simprr ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑔 ⊆ 𝑓 ) ) → 𝑔 ⊆ 𝑓 )
17 fclsss2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑔 ⊆ 𝑓 ) → ( 𝐽 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑔 ) )
18 14 15 16 17 syl3anc ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑔 ⊆ 𝑓 ) ) → ( 𝐽 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑔 ) )
19 ssn0 ⊢ ( ( ( 𝐽 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑔 ) ∧ ( 𝐽 fClus 𝑓 ) ≠ ∅ ) → ( 𝐽 fClus 𝑔 ) ≠ ∅ )
20 19 ex ⊢ ( ( 𝐽 fClus 𝑓 ) ⊆ ( 𝐽 fClus 𝑔 ) → ( ( 𝐽 fClus 𝑓 ) ≠ ∅ → ( 𝐽 fClus 𝑔 ) ≠ ∅ ) )
21 18 20 syl ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑔 ⊆ 𝑓 ) ) → ( ( 𝐽 fClus 𝑓 ) ≠ ∅ → ( 𝐽 fClus 𝑔 ) ≠ ∅ ) )
22 21 expr ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → ( 𝑔 ⊆ 𝑓 → ( ( 𝐽 fClus 𝑓 ) ≠ ∅ → ( 𝐽 fClus 𝑔 ) ≠ ∅ ) ) )
23 22 impcomd ⊢ ( ( ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → ( ( ( 𝐽 fClus 𝑓 ) ≠ ∅ ∧ 𝑔 ⊆ 𝑓 ) → ( 𝐽 fClus 𝑔 ) ≠ ∅ ) )
24 23 rexlimdva ⊢ ( ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) → ( ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( ( 𝐽 fClus 𝑓 ) ≠ ∅ ∧ 𝑔 ⊆ 𝑓 ) → ( 𝐽 fClus 𝑔 ) ≠ ∅ ) )
25 13 24 syl5 ⊢ ( ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) → ( ( ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fClus 𝑓 ) ≠ ∅ ∧ ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) 𝑔 ⊆ 𝑓 ) → ( 𝐽 fClus 𝑔 ) ≠ ∅ ) )
26 12 25 mpan2d ⊢ ( ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑔 ∈ ( Fil ‘ 𝑋 ) ) → ( ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fClus 𝑓 ) ≠ ∅ → ( 𝐽 fClus 𝑔 ) ≠ ∅ ) )
27 26 ralrimdva ⊢ ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fClus 𝑓 ) ≠ ∅ → ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐽 fClus 𝑔 ) ≠ ∅ ) )
28 fclscmp ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Comp ↔ ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐽 fClus 𝑔 ) ≠ ∅ ) )
29 28 adantl ⊢ ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝐽 ∈ Comp ↔ ∀ 𝑔 ∈ ( Fil ‘ 𝑋 ) ( 𝐽 fClus 𝑔 ) ≠ ∅ ) )
30 27 29 sylibrd ⊢ ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fClus 𝑓 ) ≠ ∅ → 𝐽 ∈ Comp ) )
31 10 30 impbid ⊢ ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝐽 ∈ Comp ↔ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fClus 𝑓 ) ≠ ∅ ) )
32 uffclsflim ⊢ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) → ( 𝐽 fClus 𝑓 ) = ( 𝐽 fLim 𝑓 ) )
33 32 neeq1d ⊢ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) → ( ( 𝐽 fClus 𝑓 ) ≠ ∅ ↔ ( 𝐽 fLim 𝑓 ) ≠ ∅ ) )
34 33 ralbiia ⊢ ( ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fClus 𝑓 ) ≠ ∅ ↔ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ )
35 31 34 bitrdi ⊢ ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝐽 ∈ Comp ↔ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ ) )