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	$$⊢\underset{cn}{⟶}=\left(a\in 𝒫ℂ,b\in 𝒫ℂ⟼\left\{f\in \left(b^a\right)|\forall x\in a\forall e\in {ℝ}^{+}\exists d\in {ℝ}^{+}\forall y\in a\left(\left|x-y\right|<d\to \left|f\left(x\right)-f\left(y\right)\right|<e\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccncf	$$class\underset{cn}{⟶}$$
1		va	$$setvara$$
2		cc	$$classℂ$$
3	2	cpw	$$class𝒫ℂ$$
4		vb	$$setvarb$$
5		vf	$$setvarf$$
6	4	cv	$$setvarb$$
7		cmap	$$class{\uparrow }_{𝑚}$$
8	1	cv	$$setvara$$
9	6 8 7	co	$$class\left(b^a\right)$$
10		vx	$$setvarx$$
11		ve	$$setvare$$
12		crp	$$class{ℝ}^{+}$$
13		vd	$$setvard$$
14		vy	$$setvary$$
15		cabs	$$class\mathrm{abs}$$
16	10	cv	$$setvarx$$
17		cmin	$$class-$$
18	14	cv	$$setvary$$
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	$$setvard$$
23	20 22 21	wbr	$$wff\left|x-y\right|<d$$
24	5	cv	$$setvarf$$
25	16 24	cfv	$$classf\left(x\right)$$
26	18 24	cfv	$$classf\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	$$setvare$$
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\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 {ℝ}^{+}\forall y\in a\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 {ℝ}^{+}\exists d\in {ℝ}^{+}\forall y\in a\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\forall e\in {ℝ}^{+}\exists d\in {ℝ}^{+}\forall y\in a\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\forall e\in {ℝ}^{+}\exists d\in {ℝ}^{+}\forall y\in a\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\forall e\in {ℝ}^{+}\exists d\in {ℝ}^{+}\forall y\in a\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	$$wff\underset{cn}{⟶}=\left(a\in 𝒫ℂ,b\in 𝒫ℂ⟼\left\{f\in \left(b^a\right)|\forall x\in a\forall e\in {ℝ}^{+}\exists d\in {ℝ}^{+}\forall y\in a\left(\left|x-y\right|<d\to \left|f\left(x\right)-f\left(y\right)\right|<e\right)\right\}\right)$$