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 𝐹 ) )