Metamath Proof Explorer

Theorem flfval

Description: Given a function from a filtered set to a topological space, define the set of limit points of the function. (Contributed by Jeff Hankins, 8-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

		Ref	Expression
	Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		toponmax	$⊢ J \in TopOn (X) \to X \in J$
2		filtop	$⊢ L \in Fil (Y) \to Y \in L$
3		elmapg	$⊢ (X \in J \land Y \in L) \to (F \in (X^{Y}) \leftrightarrow F : Y ⟶ X)$
4	1 2 3	syl2an	$⊢ (J \in TopOn (X) \land L \in Fil (Y)) \to (F \in (X^{Y}) \leftrightarrow F : Y ⟶ X)$
5	4	biimpar	$⊢ ((J \in TopOn (X) \land L \in Fil (Y)) \land F : Y ⟶ X) \to F \in (X^{Y})$
6		flffval	$⊢ (J \in TopOn (X) \land L \in Fil (Y)) \to J fLimf L = (f \in (X^{Y}) ⟼ J fLim (X FilMap f) (L))$
7	6	fveq1d	$⊢ (J \in TopOn (X) \land L \in Fil (Y)) \to (J fLimf L) (F) = (f \in (X^{Y}) ⟼ J fLim (X FilMap f) (L)) (F)$
8		oveq2	$⊢ f = F \to X FilMap f = X FilMap F$
9	8	fveq1d	$⊢ f = F \to (X FilMap f) (L) = (X FilMap F) (L)$
10	9	oveq2d	$⊢ f = F \to J fLim (X FilMap f) (L) = J fLim (X FilMap F) (L)$
11		eqid	$⊢ (f \in (X^{Y}) ⟼ J fLim (X FilMap f) (L)) = (f \in (X^{Y}) ⟼ J fLim (X FilMap f) (L))$
12		ovex	$⊢ J fLim (X FilMap F) (L) \in V$
13	10 11 12	fvmpt	$⊢ F \in (X^{Y}) \to (f \in (X^{Y}) ⟼ J fLim (X FilMap f) (L)) (F) = J fLim (X FilMap F) (L)$
14	7 13	sylan9eq	$⊢ ((J \in TopOn (X) \land L \in Fil (Y)) \land F \in (X^{Y})) \to (J fLimf L) (F) = J fLim (X FilMap F) (L)$
15	5 14	syldan	$⊢ ((J \in TopOn (X) \land L \in Fil (Y)) \land F : Y ⟶ X) \to (J fLimf L) (F) = J fLim (X FilMap F) (L)$
16	15	3impa	$⊢ (J \in TopOn (X) \land L \in Fil (Y) \land F : Y ⟶ X) \to (J fLimf L) (F) = J fLim (X FilMap F) (L)$