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$$