Theorem cncfval

Description: The value of the continuous complex function operation is the set of continuous functions from A to B . (Contributed by Paul Chapman, 11-Oct-2007) (Revised by Mario Carneiro, 9-Nov-2013)

	Ref	Expression
Assertion	cncfval	$$⊢\left(A\subseteq ℂ\wedge B\subseteq ℂ\right)\to A\underset{cn}{⟶}B=\left\{f\in \left(B^A\right)|\forall x\in A\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in A\left(\left|x-w\right|<z\to \left|f\left(x\right)-f\left(w\right)\right|<y\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		cnex	$$⊢ℂ\in \mathrm{V}$$
2	1	elpw2	$$⊢A\in 𝒫ℂ\leftrightarrow A\subseteq ℂ$$
3	1	elpw2	$$⊢B\in 𝒫ℂ\leftrightarrow B\subseteq ℂ$$
4		oveq2	$$⊢a=A\to b^a=b^A$$
5		raleq	$$⊢a=A\to \left(\forall w\in a\left(\left|x-w\right|<z\to \left|f\left(x\right)-f\left(w\right)\right|<y\right)\leftrightarrow \forall w\in A\left(\left|x-w\right|<z\to \left|f\left(x\right)-f\left(w\right)\right|<y\right)\right)$$
6	5	rexbidv	$$⊢a=A\to \left(\exists z\in {ℝ}^{+}\forall w\in a\left(\left|x-w\right|<z\to \left|f\left(x\right)-f\left(w\right)\right|<y\right)\leftrightarrow \exists z\in {ℝ}^{+}\forall w\in A\left(\left|x-w\right|<z\to \left|f\left(x\right)-f\left(w\right)\right|<y\right)\right)$$
7	6	ralbidv	$$⊢a=A\to \left(\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in a\left(\left|x-w\right|<z\to \left|f\left(x\right)-f\left(w\right)\right|<y\right)\leftrightarrow \forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in A\left(\left|x-w\right|<z\to \left|f\left(x\right)-f\left(w\right)\right|<y\right)\right)$$
8	7	raleqbi1dv	$$⊢a=A\to \left(\forall x\in a\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in a\left(\left|x-w\right|<z\to \left|f\left(x\right)-f\left(w\right)\right|<y\right)\leftrightarrow \forall x\in A\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in A\left(\left|x-w\right|<z\to \left|f\left(x\right)-f\left(w\right)\right|<y\right)\right)$$
9	4 8	rabeqbidv	$$⊢a=A\to \left\{f\in \left(b^a\right)|\forall x\in a\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in a\left(\left|x-w\right|<z\to \left|f\left(x\right)-f\left(w\right)\right|<y\right)\right\}=\left\{f\in \left(b^A\right)|\forall x\in A\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in A\left(\left|x-w\right|<z\to \left|f\left(x\right)-f\left(w\right)\right|<y\right)\right\}$$
10		oveq1	$$⊢b=B\to b^A=B^A$$
11	10	rabeqdv	$$⊢b=B\to \left\{f\in \left(b^A\right)|\forall x\in A\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in A\left(\left|x-w\right|<z\to \left|f\left(x\right)-f\left(w\right)\right|<y\right)\right\}=\left\{f\in \left(B^A\right)|\forall x\in A\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in A\left(\left|x-w\right|<z\to \left|f\left(x\right)-f\left(w\right)\right|<y\right)\right\}$$
12		df-cncf	$$⊢\underset{cn}{⟶}=\left(a\in 𝒫ℂ,b\in 𝒫ℂ⟼\left\{f\in \left(b^a\right)|\forall x\in a\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in a\left(\left|x-w\right|<z\to \left|f\left(x\right)-f\left(w\right)\right|<y\right)\right\}\right)$$
13		ovex	$$⊢B^A\in \mathrm{V}$$
14	13	rabex	$$⊢\left\{f\in \left(B^A\right)|\forall x\in A\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in A\left(\left|x-w\right|<z\to \left|f\left(x\right)-f\left(w\right)\right|<y\right)\right\}\in \mathrm{V}$$
15	9 11 12 14	ovmpo	$$⊢\left(A\in 𝒫ℂ\wedge B\in 𝒫ℂ\right)\to A\underset{cn}{⟶}B=\left\{f\in \left(B^A\right)|\forall x\in A\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in A\left(\left|x-w\right|<z\to \left|f\left(x\right)-f\left(w\right)\right|<y\right)\right\}$$
16	2 3 15	syl2anbr	$$⊢\left(A\subseteq ℂ\wedge B\subseteq ℂ\right)\to A\underset{cn}{⟶}B=\left\{f\in \left(B^A\right)|\forall x\in A\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in A\left(\left|x-w\right|<z\to \left|f\left(x\right)-f\left(w\right)\right|<y\right)\right\}$$