This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cncff

Description: A continuous complex function's domain and codomain. (Contributed by Paul Chapman, 17-Jan-2008) (Revised by Mario Carneiro, 25-Aug-2014)

		Ref	Expression
	Assertion	cncff	$⊢ F : A \underset{cn}{⟶} B \to F : A ⟶ B$

Proof

Step	Hyp	Ref	Expression
1		cncfrss	$⊢ F : A \underset{cn}{⟶} B \to A \subseteq ℂ$
2		cncfrss2	$⊢ F : A \underset{cn}{⟶} B \to B \subseteq ℂ$
3		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)))$
4	1 2 3	syl2anc	$⊢ F : A \underset{cn}{⟶} B \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)))$
5	4	ibi	$⊢ F : A \underset{cn}{⟶} B \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))$
6	5	simpld	$⊢ F : A \underset{cn}{⟶} B \to F : A ⟶ B$