# 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 ${⊢}\left({A}\subseteq ℂ\wedge {B}\subseteq ℂ\right)\to \left({F}:{A}\underset{cn}{⟶}{B}↔\left({F}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\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}↔\left({F}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\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}$