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 syl5ibr ( ( 𝑋 ∈ 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 𝑓 ) ≠ ∅ ) )