Metamath Proof Explorer

Theorem cnpval

Description: The set of all functions from topology J to topology K that are continuous at a point P . (Contributed by NM, 17-Oct-2006) (Revised by Mario Carneiro, 11-Nov-2013)

		Ref	Expression
	Assertion	cnpval	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \to (J CnP K) (P) = \{f \in (Y^{X}) \| \forall y \in K (f (P) \in y \to \exists x \in J (P \in x \land f [x] \subseteq y))\}$

Proof

Step	Hyp	Ref	Expression
1		cnpfval	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to J CnP K = (v \in X ⟼ \{f \in (Y^{X}) \| \forall y \in K (f (v) \in y \to \exists x \in J (v \in x \land f [x] \subseteq y))\})$
2	1	fveq1d	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (J CnP K) (P) = (v \in X ⟼ \{f \in (Y^{X}) \| \forall y \in K (f (v) \in y \to \exists x \in J (v \in x \land f [x] \subseteq y))\}) (P)$
3		fveq2	$⊢ v = P \to f (v) = f (P)$
4	3	eleq1d	$⊢ v = P \to (f (v) \in y \leftrightarrow f (P) \in y)$
5		eleq1	$⊢ v = P \to (v \in x \leftrightarrow P \in x)$
6	5	anbi1d	$⊢ v = P \to ((v \in x \land f [x] \subseteq y) \leftrightarrow (P \in x \land f [x] \subseteq y))$
7	6	rexbidv	$⊢ v = P \to (\exists x \in J (v \in x \land f [x] \subseteq y) \leftrightarrow \exists x \in J (P \in x \land f [x] \subseteq y))$
8	4 7	imbi12d	$⊢ v = P \to ((f (v) \in y \to \exists x \in J (v \in x \land f [x] \subseteq y)) \leftrightarrow (f (P) \in y \to \exists x \in J (P \in x \land f [x] \subseteq y)))$
9	8	ralbidv	$⊢ v = P \to (\forall y \in K (f (v) \in y \to \exists x \in J (v \in x \land f [x] \subseteq y)) \leftrightarrow \forall y \in K (f (P) \in y \to \exists x \in J (P \in x \land f [x] \subseteq y)))$
10	9	rabbidv	$⊢ v = P \to \{f \in (Y^{X}) \| \forall y \in K (f (v) \in y \to \exists x \in J (v \in x \land f [x] \subseteq y))\} = \{f \in (Y^{X}) \| \forall y \in K (f (P) \in y \to \exists x \in J (P \in x \land f [x] \subseteq y))\}$
11		eqid	$⊢ (v \in X ⟼ \{f \in (Y^{X}) \| \forall y \in K (f (v) \in y \to \exists x \in J (v \in x \land f [x] \subseteq y))\}) = (v \in X ⟼ \{f \in (Y^{X}) \| \forall y \in K (f (v) \in y \to \exists x \in J (v \in x \land f [x] \subseteq y))\})$
12		ovex	$⊢ Y^{X} \in V$
13	12	rabex	$⊢ \{f \in (Y^{X}) \| \forall y \in K (f (P) \in y \to \exists x \in J (P \in x \land f [x] \subseteq y))\} \in V$
14	10 11 13	fvmpt	$⊢ P \in X \to (v \in X ⟼ \{f \in (Y^{X}) \| \forall y \in K (f (v) \in y \to \exists x \in J (v \in x \land f [x] \subseteq y))\}) (P) = \{f \in (Y^{X}) \| \forall y \in K (f (P) \in y \to \exists x \in J (P \in x \land f [x] \subseteq y))\}$
15	2 14	sylan9eq	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land P \in X) \to (J CnP K) (P) = \{f \in (Y^{X}) \| \forall y \in K (f (P) \in y \to \exists x \in J (P \in x \land f [x] \subseteq y))\}$
16	15	3impa	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \to (J CnP K) (P) = \{f \in (Y^{X}) \| \forall y \in K (f (P) \in y \to \exists x \in J (P \in x \land f [x] \subseteq y))\}$