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	$⊢ (J \in TopOn (X) \land L \in UFil (Y) \land F : Y ⟶ X) \to (J fClusf L) (F) = (J fLimf L) (F)$

Proof

Step	Hyp	Ref	Expression
1		toponmax	$⊢ J \in TopOn (X) \to X \in J$
2		fmufil	$⊢ (X \in J \land L \in UFil (Y) \land F : Y ⟶ X) \to (X FilMap F) (L) \in UFil (X)$
3	1 2	syl3an1	$⊢ (J \in TopOn (X) \land L \in UFil (Y) \land F : Y ⟶ X) \to (X FilMap F) (L) \in UFil (X)$
4		uffclsflim	$⊢ (X FilMap F) (L) \in UFil (X) \to J fClus (X FilMap F) (L) = J fLim (X FilMap F) (L)$
5	3 4	syl	$⊢ (J \in TopOn (X) \land L \in UFil (Y) \land F : Y ⟶ X) \to J fClus (X FilMap F) (L) = J fLim (X FilMap F) (L)$
6		ufilfil	$⊢ L \in UFil (Y) \to L \in Fil (Y)$
7		fcfval	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (J fClusf L) (F) = J fClus (X FilMap F) (L)$
8	6 7	syl3an2	$⊢ (J \in TopOn (X) \land L \in UFil (Y) \land F : Y ⟶ X) \to (J fClusf L) (F) = J fClus (X FilMap F) (L)$
9		flfval	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (J fLimf L) (F) = J fLim (X FilMap F) (L)$
10	6 9	syl3an2	$⊢ (J \in TopOn (X) \land L \in UFil (Y) \land F : Y ⟶ X) \to (J fLimf L) (F) = J fLim (X FilMap F) (L)$
11	5 8 10	3eqtr4d	$⊢ (J \in TopOn (X) \land L \in UFil (Y) \land F : Y ⟶ X) \to (J fClusf L) (F) = (J fLimf L) (F)$