# Metamath Proof Explorer

## Theorem cncffvrn

Description: Change the codomain of a continuous complex function. (Contributed by Paul Chapman, 18-Oct-2007) (Revised by Mario Carneiro, 1-May-2015)

Ref Expression
Assertion cncffvrn ${⊢}\left({C}\subseteq ℂ\wedge {F}:{A}\underset{cn}{⟶}{B}\right)\to \left({F}:{A}\underset{cn}{⟶}{C}↔{F}:{A}⟶{C}\right)$

### Proof

Step Hyp Ref Expression
1 cncfi ${⊢}\left({F}:{A}\underset{cn}{⟶}{B}\wedge {x}\in {A}\wedge {y}\in {ℝ}^{+}\right)\to \exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left|{w}-{x}\right|<{z}\to \left|{F}\left({w}\right)-{F}\left({x}\right)\right|<{y}\right)$
2 1 3expb ${⊢}\left({F}:{A}\underset{cn}{⟶}{B}\wedge \left({x}\in {A}\wedge {y}\in {ℝ}^{+}\right)\right)\to \exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left|{w}-{x}\right|<{z}\to \left|{F}\left({w}\right)-{F}\left({x}\right)\right|<{y}\right)$
3 2 ralrimivva ${⊢}{F}:{A}\underset{cn}{⟶}{B}\to \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|{w}-{x}\right|<{z}\to \left|{F}\left({w}\right)-{F}\left({x}\right)\right|<{y}\right)$
4 3 adantl ${⊢}\left({C}\subseteq ℂ\wedge {F}:{A}\underset{cn}{⟶}{B}\right)\to \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|{w}-{x}\right|<{z}\to \left|{F}\left({w}\right)-{F}\left({x}\right)\right|<{y}\right)$
5 cncfrss ${⊢}{F}:{A}\underset{cn}{⟶}{B}\to {A}\subseteq ℂ$
6 simpl ${⊢}\left({C}\subseteq ℂ\wedge {F}:{A}\underset{cn}{⟶}{B}\right)\to {C}\subseteq ℂ$
7 elcncf2 ${⊢}\left({A}\subseteq ℂ\wedge {C}\subseteq ℂ\right)\to \left({F}:{A}\underset{cn}{⟶}{C}↔\left({F}:{A}⟶{C}\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|{w}-{x}\right|<{z}\to \left|{F}\left({w}\right)-{F}\left({x}\right)\right|<{y}\right)\right)\right)$
8 5 6 7 syl2an2 ${⊢}\left({C}\subseteq ℂ\wedge {F}:{A}\underset{cn}{⟶}{B}\right)\to \left({F}:{A}\underset{cn}{⟶}{C}↔\left({F}:{A}⟶{C}\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|{w}-{x}\right|<{z}\to \left|{F}\left({w}\right)-{F}\left({x}\right)\right|<{y}\right)\right)\right)$
9 4 8 mpbiran2d ${⊢}\left({C}\subseteq ℂ\wedge {F}:{A}\underset{cn}{⟶}{B}\right)\to \left({F}:{A}\underset{cn}{⟶}{C}↔{F}:{A}⟶{C}\right)$