flffval

Description: Given a topology and a filtered set, return the convergence function on the functions from the filtered set to the base set of the topological space. (Contributed by Jeff Hankins, 14-Oct-2009) (Revised by Mario Carneiro, 15-Dec-2013) (Revised by Stefan O'Rear, 6-Aug-2015)

		Ref	Expression
	Assertion	flffval	$⊢ (J \in TopOn (X) \land L \in Fil (Y)) \to J fLimf L = (f \in (X^{Y}) ⟼ J fLim (X FilMap f) (L))$

Proof

Step	Hyp	Ref	Expression
1		topontop	$⊢ J \in TopOn (X) \to J \in Top$
2		fvssunirn	$⊢ Fil (Y) \subseteq ⋃ ran Fil$
3	2	sseli	$⊢ L \in Fil (Y) \to L \in ⋃ ran Fil$
4		unieq	$⊢ x = J \to ⋃ x = ⋃ J$
5		unieq	$⊢ y = L \to ⋃ y = ⋃ L$
6	4 5	oveqan12d	$⊢ (x = J \land y = L) \to {⋃ x}^{⋃ y} = {⋃ J}^{⋃ L}$
7		simpl	$⊢ (x = J \land y = L) \to x = J$
8	4	adantr	$⊢ (x = J \land y = L) \to ⋃ x = ⋃ J$
9	8	oveq1d	$⊢ (x = J \land y = L) \to ⋃ x FilMap f = ⋃ J FilMap f$
10		simpr	$⊢ (x = J \land y = L) \to y = L$
11	9 10	fveq12d	$⊢ (x = J \land y = L) \to (⋃ x FilMap f) (y) = (⋃ J FilMap f) (L)$
12	7 11	oveq12d	$⊢ (x = J \land y = L) \to x fLim (⋃ x FilMap f) (y) = J fLim (⋃ J FilMap f) (L)$
13	6 12	mpteq12dv	$⊢ (x = J \land y = L) \to (f \in ({⋃ x}^{⋃ y}) ⟼ x fLim (⋃ x FilMap f) (y)) = (f \in ({⋃ J}^{⋃ L}) ⟼ J fLim (⋃ J FilMap f) (L))$
14		df-flf	$⊢ fLimf = (x \in Top, y \in ⋃ ran Fil ⟼ (f \in ({⋃ x}^{⋃ y}) ⟼ x fLim (⋃ x FilMap f) (y)))$
15		ovex	$⊢ {⋃ J}^{⋃ L} \in V$
16	15	mptex	$⊢ (f \in ({⋃ J}^{⋃ L}) ⟼ J fLim (⋃ J FilMap f) (L)) \in V$
17	13 14 16	ovmpoa	$⊢ (J \in Top \land L \in ⋃ ran Fil) \to J fLimf L = (f \in ({⋃ J}^{⋃ L}) ⟼ J fLim (⋃ J FilMap f) (L))$
18	1 3 17	syl2an	$⊢ (J \in TopOn (X) \land L \in Fil (Y)) \to J fLimf L = (f \in ({⋃ J}^{⋃ L}) ⟼ J fLim (⋃ J FilMap f) (L))$
19		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
20	19	eqcomd	$⊢ J \in TopOn (X) \to ⋃ J = X$
21		filunibas	$⊢ L \in Fil (Y) \to ⋃ L = Y$
22	20 21	oveqan12d	$⊢ (J \in TopOn (X) \land L \in Fil (Y)) \to {⋃ J}^{⋃ L} = X^{Y}$
23	20	adantr	$⊢ (J \in TopOn (X) \land L \in Fil (Y)) \to ⋃ J = X$
24	23	oveq1d	$⊢ (J \in TopOn (X) \land L \in Fil (Y)) \to ⋃ J FilMap f = X FilMap f$
25	24	fveq1d	$⊢ (J \in TopOn (X) \land L \in Fil (Y)) \to (⋃ J FilMap f) (L) = (X FilMap f) (L)$
26	25	oveq2d	$⊢ (J \in TopOn (X) \land L \in Fil (Y)) \to J fLim (⋃ J FilMap f) (L) = J fLim (X FilMap f) (L)$
27	22 26	mpteq12dv	$⊢ (J \in TopOn (X) \land L \in Fil (Y)) \to (f \in ({⋃ J}^{⋃ L}) ⟼ J fLim (⋃ J FilMap f) (L)) = (f \in (X^{Y}) ⟼ J fLim (X FilMap f) (L))$
28	18 27	eqtrd	$⊢ (J \in TopOn (X) \land L \in Fil (Y)) \to J fLimf L = (f \in (X^{Y}) ⟼ J fLim (X FilMap f) (L))$

Metamath Proof Explorer

Theorem flffval

Proof