Metamath Proof Explorer


Theorem uffcfflf

Description: If the domain filter is an ultrafilter, the cluster points of the function are the limit points. (Contributed by Jeff Hankins, 12-Dec-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion uffcfflf ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌𝑋 ) → ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) = ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 toponmax ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋𝐽 )
2 fmufil ( ( 𝑋𝐽𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( UFil ‘ 𝑋 ) )
3 1 2 syl3an1 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( UFil ‘ 𝑋 ) )
4 uffclsflim ( ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( UFil ‘ 𝑋 ) → ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
5 3 4 syl ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌𝑋 ) → ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
6 ufilfil ( 𝐿 ∈ ( UFil ‘ 𝑌 ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
7 fcfval ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌𝑋 ) → ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
8 6 7 syl3an2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌𝑋 ) → ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
9 flfval ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌𝑋 ) → ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
10 6 9 syl3an2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌𝑋 ) → ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fLim ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
11 5 8 10 3eqtr4d ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( UFil ‘ 𝑌 ) ∧ 𝐹 : 𝑌𝑋 ) → ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) = ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) )