Metamath Proof Explorer

Theorem elcncf1di

Description: Membership in the set of continuous complex functions from A to B . (Contributed by Paul Chapman, 26-Nov-2007)

		Ref	Expression
	Hypotheses	elcncf1d.1	$⊢ φ \to F : A ⟶ B$
		elcncf1d.2	$⊢ φ \to ((x \in A \land y \in ℝ^{+}) \to Z \in ℝ^{+})$
		elcncf1d.3	$⊢ φ \to (((x \in A \land w \in A) \land y \in ℝ^{+}) \to (\|x - w\| < Z \to \|F (x) - F (w)\| < y))$
	Assertion	elcncf1di	$⊢ φ \to ((A \subseteq ℂ \land B \subseteq ℂ) \to F : A \underset{cn}{⟶} B)$

Proof

Step	Hyp	Ref	Expression
1		elcncf1d.1	$⊢ φ \to F : A ⟶ B$
2		elcncf1d.2	$⊢ φ \to ((x \in A \land y \in ℝ^{+}) \to Z \in ℝ^{+})$
3		elcncf1d.3	$⊢ φ \to (((x \in A \land w \in A) \land y \in ℝ^{+}) \to (\|x - w\| < Z \to \|F (x) - F (w)\| < y))$
4	2	imp	$⊢ (φ \land (x \in A \land y \in ℝ^{+})) \to Z \in ℝ^{+}$
5		an32	$⊢ ((x \in A \land w \in A) \land y \in ℝ^{+}) \leftrightarrow ((x \in A \land y \in ℝ^{+}) \land w \in A)$
6	5	bianass	$⊢ (φ \land ((x \in A \land w \in A) \land y \in ℝ^{+})) \leftrightarrow ((φ \land (x \in A \land y \in ℝ^{+})) \land w \in A)$
7	3	imp	$⊢ (φ \land ((x \in A \land w \in A) \land y \in ℝ^{+})) \to (\|x - w\| < Z \to \|F (x) - F (w)\| < y)$
8	6 7	sylbir	$⊢ ((φ \land (x \in A \land y \in ℝ^{+})) \land w \in A) \to (\|x - w\| < Z \to \|F (x) - F (w)\| < y)$
9	8	ralrimiva	$⊢ (φ \land (x \in A \land y \in ℝ^{+})) \to \forall w \in A (\|x - w\| < Z \to \|F (x) - F (w)\| < y)$
10		breq2	$⊢ z = Z \to (\|x - w\| < z \leftrightarrow \|x - w\| < Z)$
11	10	rspceaimv	$⊢ (Z \in ℝ^{+} \land \forall w \in A (\|x - w\| < Z \to \|F (x) - F (w)\| < y)) \to \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|F (x) - F (w)\| < y)$
12	4 9 11	syl2anc	$⊢ (φ \land (x \in A \land y \in ℝ^{+})) \to \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|F (x) - F (w)\| < y)$
13	12	ralrimivva	$⊢ φ \to \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in A (\|x - w\| < z \to \|F (x) - F (w)\| < y)$
14	1 13	jca	$⊢ φ \to (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))$
15		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)))$
16	14 15	syl5ibrcom	$⊢ φ \to ((A \subseteq ℂ \land B \subseteq ℂ) \to F : A \underset{cn}{⟶} B)$