Metamath Proof Explorer

Theorem iscnp

Description: The predicate "the class F is a continuous function from topology J to topology K at point P ". Based on Theorem 7.2(g) of Munkres p. 107. (Contributed by NM, 17-Oct-2006) (Revised by Mario Carneiro, 21-Aug-2015)

		Ref	Expression
	Assertion	iscnp	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \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		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))\}$
2	1	eleq2d	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow F \in \{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))\})$
3		fveq1	$⊢ f = F \to f (P) = F (P)$
4	3	eleq1d	$⊢ f = F \to (f (P) \in y \leftrightarrow F (P) \in y)$
5		imaeq1	$⊢ f = F \to f [x] = F [x]$
6	5	sseq1d	$⊢ f = F \to (f [x] \subseteq y \leftrightarrow F [x] \subseteq y)$
7	6	anbi2d	$⊢ f = F \to ((P \in x \land f [x] \subseteq y) \leftrightarrow (P \in x \land F [x] \subseteq y))$
8	7	rexbidv	$⊢ f = F \to (\exists x \in J (P \in x \land f [x] \subseteq y) \leftrightarrow \exists x \in J (P \in x \land F [x] \subseteq y))$
9	4 8	imbi12d	$⊢ f = F \to ((f (P) \in y \to \exists x \in J (P \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)))$
10	9	ralbidv	$⊢ f = F \to (\forall y \in K (f (P) \in y \to \exists x \in J (P \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)))$
11	10	elrab	$⊢ F \in \{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))\} \leftrightarrow (F \in (Y^{X}) \land \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y)))$
12		toponmax	$⊢ K \in TopOn (Y) \to Y \in K$
13		toponmax	$⊢ J \in TopOn (X) \to X \in J$
14		elmapg	$⊢ (Y \in K \land X \in J) \to (F \in (Y^{X}) \leftrightarrow F : X ⟶ Y)$
15	12 13 14	syl2anr	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (Y^{X}) \leftrightarrow F : X ⟶ Y)$
16	15	anbi1d	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to ((F \in (Y^{X}) \land \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))) \leftrightarrow (F : X ⟶ Y \land \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))))$
17	11 16	syl5bb	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in \{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))\} \leftrightarrow (F : X ⟶ Y \land \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))))$
18	17	3adant3	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \to (F \in \{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))\} \leftrightarrow (F : X ⟶ Y \land \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))))$
19	2 18	bitrd	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall y \in K (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))))$