Metamath Proof Explorer

Theorem elcncf

Description: Membership in the set of continuous complex functions from A to B . (Contributed by Paul Chapman, 11-Oct-2007) (Revised by Mario Carneiro, 9-Nov-2013)

		Ref	Expression
	Assertion	elcncf	$⊢ (A \subseteq ℂ \land B \subseteq ℂ) \to (F : A \underset{cn}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|F (x) - F (w)\| < y)))$

Proof

Step	Hyp	Ref	Expression
1		cncfval	$⊢ (A \subseteq ℂ \land B \subseteq ℂ) \to A \underset{cn}{⟶} B = \{f \in (B^{A}) \| \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|f (x) - f (w)\| < y)\}$
2	1	eleq2d	$⊢ (A \subseteq ℂ \land B \subseteq ℂ) \to (F : A \underset{cn}{⟶} B \leftrightarrow F \in \{f \in (B^{A}) \| \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|f (x) - f (w)\| < y)\})$
3		fveq1	$⊢ f = F \to f (x) = F (x)$
4		fveq1	$⊢ f = F \to f (w) = F (w)$
5	3 4	oveq12d	$⊢ f = F \to f (x) - f (w) = F (x) - F (w)$
6	5	fveq2d	$⊢ f = F \to \|f (x) - f (w)\| = \|F (x) - F (w)\|$
7	6	breq1d	$⊢ f = F \to (\|f (x) - f (w)\| < y \leftrightarrow \|F (x) - F (w)\| < y)$
8	7	imbi2d	$⊢ f = F \to ((\|x - w\| < z \to \|f (x) - f (w)\| < y) \leftrightarrow (\|x - w\| < z \to \|F (x) - F (w)\| < y))$
9	8	rexralbidv	$⊢ f = F \to (\exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|f (x) - f (w)\| < y) \leftrightarrow \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|F (x) - F (w)\| < y))$
10	9	2ralbidv	$⊢ f = F \to (\forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|f (x) - f (w)\| < y) \leftrightarrow \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|F (x) - F (w)\| < y))$
11	10	elrab	$⊢ F \in \{f \in (B^{A}) \| \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|f (x) - f (w)\| < y)\} \leftrightarrow (F \in (B^{A}) \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|F (x) - F (w)\| < y))$
12	2 11	bitrdi	$⊢ (A \subseteq ℂ \land B \subseteq ℂ) \to (F : A \underset{cn}{⟶} B \leftrightarrow (F \in (B^{A}) \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|F (x) - F (w)\| < y)))$
13		cnex	$⊢ ℂ \in V$
14	13	ssex	$⊢ B \subseteq ℂ \to B \in V$
15	13	ssex	$⊢ A \subseteq ℂ \to A \in V$
16		elmapg	$⊢ (B \in V \land A \in V) \to (F \in (B^{A}) \leftrightarrow F : A ⟶ B)$
17	14 15 16	syl2anr	$⊢ (A \subseteq ℂ \land B \subseteq ℂ) \to (F \in (B^{A}) \leftrightarrow F : A ⟶ B)$
18	17	anbi1d	$⊢ (A \subseteq ℂ \land B \subseteq ℂ) \to ((F \in (B^{A}) \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|F (x) - F (w)\| < y)) \leftrightarrow (F : A ⟶ B \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|F (x) - F (w)\| < y)))$
19	12 18	bitrd	$⊢ (A \subseteq ℂ \land B \subseteq ℂ) \to (F : A \underset{cn}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|F (x) - F (w)\| < y)))$