elcncf1ii

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

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

Step	Hyp	Ref	Expression
1		elcncf1i.1	$⊢ F : A ⟶ B$
2		elcncf1i.2	$⊢ (x \in A \land y \in ℝ^{+}) \to Z \in ℝ^{+}$
3		elcncf1i.3	$⊢ ((x \in A \land w \in A) \land y \in ℝ^{+}) \to (\|x - w\| < Z \to \|F (x) - F (w)\| < y)$
4	1	a1i	$⊢ ⊤ \to F : A ⟶ B$
5	2	a1i	$⊢ ⊤ \to ((x \in A \land y \in ℝ^{+}) \to Z \in ℝ^{+})$
6	3	a1i	$⊢ ⊤ \to (((x \in A \land w \in A) \land y \in ℝ^{+}) \to (\|x - w\| < Z \to \|F (x) - F (w)\| < y))$
7	4 5 6	elcncf1di	$⊢ ⊤ \to ((A \subseteq ℂ \land B \subseteq ℂ) \to F : A \underset{cn}{⟶} B)$
8	7	mptru	$⊢ (A \subseteq ℂ \land B \subseteq ℂ) \to F : A \underset{cn}{⟶} B$

Metamath Proof Explorer