# Metamath Proof Explorer

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

### Proof

Step Hyp Ref Expression
1 cnex ${⊢}ℂ\in \mathrm{V}$
2 1 elpw2 ${⊢}{A}\in 𝒫ℂ↔{A}\subseteq ℂ$
3 1 elpw2 ${⊢}{B}\in 𝒫ℂ↔{B}\subseteq ℂ$
4 oveq2 ${⊢}{a}={A}\to {{b}}^{{a}}={{b}}^{{A}}$
5 raleq ${⊢}{a}={A}\to \left(\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)↔\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)$
6 5 rexbidv ${⊢}{a}={A}\to \left(\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)↔\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)$
7 6 ralbidv ${⊢}{a}={A}\to \left(\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)↔\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)$
8 7 raleqbi1dv ${⊢}{a}={A}\to \left(\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)↔\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)$
9 4 8 rabeqbidv ${⊢}{a}={A}\to \left\{{f}\in \left({{b}}^{{a}}\right)|\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\}=\left\{{f}\in \left({{b}}^{{A}}\right)|\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\}$
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}\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\}=\left\{{f}\in \left({{B}}^{{A}}\right)|\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\}$
12 df-cncf
13 ovex ${⊢}{{B}}^{{A}}\in \mathrm{V}$
14 13 rabex ${⊢}\left\{{f}\in \left({{B}}^{{A}}\right)|\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\}\in \mathrm{V}$
15 9 11 12 14 ovmpo
16 2 3 15 syl2anbr