# Metamath Proof Explorer

## Theorem elcncf1ii

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

Ref Expression
Hypotheses elcncf1i.1 ${⊢}{F}:{A}⟶{B}$
elcncf1i.2 ${⊢}\left({x}\in {A}\wedge {y}\in {ℝ}^{+}\right)\to {Z}\in {ℝ}^{+}$
elcncf1i.3 ${⊢}\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)$
Assertion elcncf1ii ${⊢}\left({A}\subseteq ℂ\wedge {B}\subseteq ℂ\right)\to {F}:{A}\underset{cn}{⟶}{B}$

### Proof

Step Hyp Ref Expression
1 elcncf1i.1 ${⊢}{F}:{A}⟶{B}$
2 elcncf1i.2 ${⊢}\left({x}\in {A}\wedge {y}\in {ℝ}^{+}\right)\to {Z}\in {ℝ}^{+}$
3 elcncf1i.3 ${⊢}\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)$
4 1 a1i ${⊢}\top \to {F}:{A}⟶{B}$
5 2 a1i ${⊢}\top \to \left(\left({x}\in {A}\wedge {y}\in {ℝ}^{+}\right)\to {Z}\in {ℝ}^{+}\right)$
6 3 a1i ${⊢}\top \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)$
7 4 5 6 elcncf1di ${⊢}\top \to \left(\left({A}\subseteq ℂ\wedge {B}\subseteq ℂ\right)\to {F}:{A}\underset{cn}{⟶}{B}\right)$
8 7 mptru ${⊢}\left({A}\subseteq ℂ\wedge {B}\subseteq ℂ\right)\to {F}:{A}\underset{cn}{⟶}{B}$