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 ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐽 fClus 𝐹 ) = ( 𝐽 fLim 𝐹 ) )

Proof

Step Hyp Ref Expression
1 ufilfil ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
2 fclsfnflim ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ↔ ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) )
3 1 2 syl ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ↔ ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) )
4 3 biimpa ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) → ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) )
5 simprrr ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝑥 ∈ ( 𝐽 fLim 𝑓 ) )
6 simpll ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝐹 ∈ ( UFil ‘ 𝑋 ) )
7 simprl ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) )
8 simprrl ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝐹 ⊆ 𝑓 )
9 ufilmax ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝑓 ) → 𝐹 = 𝑓 )
10 6 7 8 9 syl3anc ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝐹 = 𝑓 )
11 10 oveq2d ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → ( 𝐽 fLim 𝐹 ) = ( 𝐽 fLim 𝑓 ) )
12 5 11 eleqtrrd ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐹 ⊆ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝑥 ∈ ( 𝐽 fLim 𝐹 ) )
13 4 12 rexlimddv ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝑥 ∈ ( 𝐽 fLim 𝐹 ) )
14 13 ex ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝐽 fClus 𝐹 ) → 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) )
15 14 ssrdv ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐽 fClus 𝐹 ) ⊆ ( 𝐽 fLim 𝐹 ) )
16 flimfcls ⊢ ( 𝐽 fLim 𝐹 ) ⊆ ( 𝐽 fClus 𝐹 )
17 16 a1i ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐽 fLim 𝐹 ) ⊆ ( 𝐽 fClus 𝐹 ) )
18 15 17 eqssd ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐽 fClus 𝐹 ) = ( 𝐽 fLim 𝐹 ) )