# Metamath Proof Explorer

## Theorem elcncf1di

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

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

### Proof

Step Hyp Ref Expression
1 elcncf1d.1 ${⊢}{\phi }\to {F}:{A}⟶{B}$
2 elcncf1d.2 ${⊢}{\phi }\to \left(\left({x}\in {A}\wedge {y}\in {ℝ}^{+}\right)\to {Z}\in {ℝ}^{+}\right)$
3 elcncf1d.3 ${⊢}{\phi }\to \left(\left(\left({x}\in {A}\wedge {w}\in {A}\right)\wedge {y}\in {ℝ}^{+}\right)\to \left(\left|{x}-{w}\right|<{Z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)\right)$
4 2 imp ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {ℝ}^{+}\right)\right)\to {Z}\in {ℝ}^{+}$
5 an32 ${⊢}\left(\left({x}\in {A}\wedge {w}\in {A}\right)\wedge {y}\in {ℝ}^{+}\right)↔\left(\left({x}\in {A}\wedge {y}\in {ℝ}^{+}\right)\wedge {w}\in {A}\right)$
6 5 bianass ${⊢}\left({\phi }\wedge \left(\left({x}\in {A}\wedge {w}\in {A}\right)\wedge {y}\in {ℝ}^{+}\right)\right)↔\left(\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {ℝ}^{+}\right)\right)\wedge {w}\in {A}\right)$
7 3 imp ${⊢}\left({\phi }\wedge \left(\left({x}\in {A}\wedge {w}\in {A}\right)\wedge {y}\in {ℝ}^{+}\right)\right)\to \left(\left|{x}-{w}\right|<{Z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)$
8 6 7 sylbir ${⊢}\left(\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {ℝ}^{+}\right)\right)\wedge {w}\in {A}\right)\to \left(\left|{x}-{w}\right|<{Z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)$
9 8 ralrimiva ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {ℝ}^{+}\right)\right)\to \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)$
10 breq2 ${⊢}{z}={Z}\to \left(\left|{x}-{w}\right|<{z}↔\left|{x}-{w}\right|<{Z}\right)$
11 10 rspceaimv ${⊢}\left({Z}\in {ℝ}^{+}\wedge \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)\to \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)$
12 4 9 11 syl2anc ${⊢}\left({\phi }\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|{x}-{w}\right|<{z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)$
13 12 ralrimivva ${⊢}{\phi }\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|{x}-{w}\right|<{z}\to \left|{F}\left({x}\right)-{F}\left({w}\right)\right|<{y}\right)$
14 1 13 jca ${⊢}{\phi }\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)$
15 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)$
16 14 15 syl5ibrcom ${⊢}{\phi }\to \left(\left({A}\subseteq ℂ\wedge {B}\subseteq ℂ\right)\to {F}:{A}\underset{cn}{⟶}{B}\right)$