Metamath Proof Explorer

Definition df-cncf

Description: Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007)

Ref Expression
Assertion df-cncf

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccncf
1 va ${setvar}{a}$
2 cc ${class}ℂ$
3 2 cpw ${class}𝒫ℂ$
4 vb ${setvar}{b}$
5 vf ${setvar}{f}$
6 4 cv ${setvar}{b}$
7 cmap ${class}{↑}_{𝑚}$
8 1 cv ${setvar}{a}$
9 6 8 7 co ${class}\left({{b}}^{{a}}\right)$
10 vx ${setvar}{x}$
11 ve ${setvar}{e}$
12 crp ${class}{ℝ}^{+}$
13 vd ${setvar}{d}$
14 vy ${setvar}{y}$
15 cabs ${class}\mathrm{abs}$
16 10 cv ${setvar}{x}$
17 cmin ${class}-$
18 14 cv ${setvar}{y}$
19 16 18 17 co ${class}\left({x}-{y}\right)$
20 19 15 cfv ${class}\left|{x}-{y}\right|$
21 clt ${class}<$
22 13 cv ${setvar}{d}$
23 20 22 21 wbr ${wff}\left|{x}-{y}\right|<{d}$
24 5 cv ${setvar}{f}$
25 16 24 cfv ${class}{f}\left({x}\right)$
26 18 24 cfv ${class}{f}\left({y}\right)$
27 25 26 17 co ${class}\left({f}\left({x}\right)-{f}\left({y}\right)\right)$
28 27 15 cfv ${class}\left|{f}\left({x}\right)-{f}\left({y}\right)\right|$
29 11 cv ${setvar}{e}$
30 28 29 21 wbr ${wff}\left|{f}\left({x}\right)-{f}\left({y}\right)\right|<{e}$
31 23 30 wi ${wff}\left(\left|{x}-{y}\right|<{d}\to \left|{f}\left({x}\right)-{f}\left({y}\right)\right|<{e}\right)$
32 31 14 8 wral ${wff}\forall {y}\in {a}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{y}\right|<{d}\to \left|{f}\left({x}\right)-{f}\left({y}\right)\right|<{e}\right)$
33 32 13 12 wrex ${wff}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in {a}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{y}\right|<{d}\to \left|{f}\left({x}\right)-{f}\left({y}\right)\right|<{e}\right)$
34 33 11 12 wral ${wff}\forall {e}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in {a}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{y}\right|<{d}\to \left|{f}\left({x}\right)-{f}\left({y}\right)\right|<{e}\right)$
35 34 10 8 wral ${wff}\forall {x}\in {a}\phantom{\rule{.4em}{0ex}}\forall {e}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in {a}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{y}\right|<{d}\to \left|{f}\left({x}\right)-{f}\left({y}\right)\right|<{e}\right)$
36 35 5 9 crab ${class}\left\{{f}\in \left({{b}}^{{a}}\right)|\forall {x}\in {a}\phantom{\rule{.4em}{0ex}}\forall {e}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in {a}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{y}\right|<{d}\to \left|{f}\left({x}\right)-{f}\left({y}\right)\right|<{e}\right)\right\}$
37 1 4 3 3 36 cmpo ${class}\left({a}\in 𝒫ℂ,{b}\in 𝒫ℂ⟼\left\{{f}\in \left({{b}}^{{a}}\right)|\forall {x}\in {a}\phantom{\rule{.4em}{0ex}}\forall {e}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {y}\in {a}\phantom{\rule{.4em}{0ex}}\left(\left|{x}-{y}\right|<{d}\to \left|{f}\left({x}\right)-{f}\left({y}\right)\right|<{e}\right)\right\}\right)$
38 0 37 wceq