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

Metamath Proof Explorer

Theorem uffclsflim

Description: The cluster points of an ultrafilter are its limit points. (Contributed by Jeff Hankins, 11-Dec-2009) (Revised by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion uffclsflim ⊢ F ∈ UFil ⁡ X → J fClus F = J fLim F

Proof

Step Hyp Ref Expression
1 ufilfil ⊢ F ∈ UFil ⁡ X → F ∈ Fil ⁡ X
2 fclsfnflim ⊢ F ∈ Fil ⁡ X → x ∈ J fClus F ↔ ∃ f ∈ Fil ⁡ X F ⊆ f ∧ x ∈ J fLim f
3 1 2 syl ⊢ F ∈ UFil ⁡ X → x ∈ J fClus F ↔ ∃ f ∈ Fil ⁡ X F ⊆ f ∧ x ∈ J fLim f
4 3 biimpa ⊢ F ∈ UFil ⁡ X ∧ x ∈ J fClus F → ∃ f ∈ Fil ⁡ X F ⊆ f ∧ x ∈ J fLim f
5 simprrr ⊢ F ∈ UFil ⁡ X ∧ x ∈ J fClus F ∧ f ∈ Fil ⁡ X ∧ F ⊆ f ∧ x ∈ J fLim f → x ∈ J fLim f
6 simpll ⊢ F ∈ UFil ⁡ X ∧ x ∈ J fClus F ∧ f ∈ Fil ⁡ X ∧ F ⊆ f ∧ x ∈ J fLim f → F ∈ UFil ⁡ X
7 simprl ⊢ F ∈ UFil ⁡ X ∧ x ∈ J fClus F ∧ f ∈ Fil ⁡ X ∧ F ⊆ f ∧ x ∈ J fLim f → f ∈ Fil ⁡ X
8 simprrl ⊢ F ∈ UFil ⁡ X ∧ x ∈ J fClus F ∧ f ∈ Fil ⁡ X ∧ F ⊆ f ∧ x ∈ J fLim f → F ⊆ f
9 ufilmax ⊢ F ∈ UFil ⁡ X ∧ f ∈ Fil ⁡ X ∧ F ⊆ f → F = f
10 6 7 8 9 syl3anc ⊢ F ∈ UFil ⁡ X ∧ x ∈ J fClus F ∧ f ∈ Fil ⁡ X ∧ F ⊆ f ∧ x ∈ J fLim f → F = f
11 10 oveq2d ⊢ F ∈ UFil ⁡ X ∧ x ∈ J fClus F ∧ f ∈ Fil ⁡ X ∧ F ⊆ f ∧ x ∈ J fLim f → J fLim F = J fLim f
12 5 11 eleqtrrd ⊢ F ∈ UFil ⁡ X ∧ x ∈ J fClus F ∧ f ∈ Fil ⁡ X ∧ F ⊆ f ∧ x ∈ J fLim f → x ∈ J fLim F
13 4 12 rexlimddv ⊢ F ∈ UFil ⁡ X ∧ x ∈ J fClus F → x ∈ J fLim F
14 13 ex ⊢ F ∈ UFil ⁡ X → x ∈ J fClus F → x ∈ J fLim F
15 14 ssrdv ⊢ F ∈ UFil ⁡ X → J fClus F ⊆ J fLim F
16 flimfcls ⊢ J fLim F ⊆ J fClus F
17 16 a1i ⊢ F ∈ UFil ⁡ X → J fLim F ⊆ J fClus F
18 15 17 eqssd ⊢ F ∈ UFil ⁡ X → J fClus F = J fLim F