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