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	$$⊢\left(A\subseteq ℂ\wedge B\subseteq ℂ\right)\to \left(F:A\underset{cn}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \forall x\in A\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in A\left(\left|x-w\right|<z\to \left|F\left(x\right)-F\left(w\right)\right|<y\right)\right)\right)$$
4	1 2 3	syl2anc	$$⊢F:A\underset{cn}{⟶}B\to \left(F:A\underset{cn}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \forall x\in A\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in A\left(\left|x-w\right|<z\to \left|F\left(x\right)-F\left(w\right)\right|<y\right)\right)\right)$$
5	4	ibi	$$⊢F:A\underset{cn}{⟶}B\to \left(F:A⟶B\wedge \forall x\in A\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in A\left(\left|x-w\right|<z\to \left|F\left(x\right)-F\left(w\right)\right|<y\right)\right)$$
6	5	simpld	$$⊢F:A\underset{cn}{⟶}B\to F:A⟶B$$