Definition df-cncf 7263

Description: Define the operation whose value is a class of continuous complex functions.

Assertion

Ref	Expression
df-cncf	|- -cn-> = {<.<.a, b>., s>. | ((a (_ CC /\ b (_ CC) /\ s = {f | (f:a-->b /\ A.x e. a A.y e. RR+ E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))})}

Distinct variable group:   a,b,f,s,x,y,z,w

Detailed syntax breakdown of Definition df-cncf

Step	Hyp	Ref	Expression
1		ccncf 7262	. 2 class -cn->
2		va	. . . . . . 7 set a
3	2	cv 955	. . . . . 6 class a
4		cc 5232	. . . . . 6 class CC
5	3, 4	wss 2047	. . . . 5 wff a (_ CC
6		vb	. . . . . . 7 set b
7	6	cv 955	. . . . . 6 class b
8	7, 4	wss 2047	. . . . 5 wff b (_ CC
9	5, 8	wa 223	. . . 4 wff (a (_ CC /\ b (_ CC)
10		vs	. . . . . 6 set s
11	10	cv 955	. . . . 5 class s
12		vf	. . . . . . . . 9 set f
13	12	cv 955	. . . . . . . 8 class f
14	3, 7, 13	wf 3178	. . . . . . 7 wff f:a-->b
15		vx	. . . . . . . . . . . . . . . 16 set x
16	15	cv 955	. . . . . . . . . . . . . . 15 class x
17		vw	. . . . . . . . . . . . . . . 16 set w
18	17	cv 955	. . . . . . . . . . . . . . 15 class w
19		cmin 5292	. . . . . . . . . . . . . . 15 class -
20	16, 18, 19	co 3963	. . . . . . . . . . . . . 14 class (x - w)
21		cabs 6750	. . . . . . . . . . . . . 14 class abs
22	20, 21	cfv 3182	. . . . . . . . . . . . 13 class (abs` (x - w))
23		vz	. . . . . . . . . . . . . 14 set z
24	23	cv 955	. . . . . . . . . . . . 13 class z
25		clt 5486	. . . . . . . . . . . . 13 class <
26	22, 24, 25	wbr 2619	. . . . . . . . . . . 12 wff (abs` (x - w)) < z
27	16, 13	cfv 3182	. . . . . . . . . . . . . . 15 class (f` x)
28	18, 13	cfv 3182	. . . . . . . . . . . . . . 15 class (f` w)
29	27, 28, 19	co 3963	. . . . . . . . . . . . . 14 class ((f` x) - (f` w))
30	29, 21	cfv 3182	. . . . . . . . . . . . 13 class (abs` ((f` x) - (f` w)))
31		vy	. . . . . . . . . . . . . 14 set y
32	31	cv 955	. . . . . . . . . . . . 13 class y
33	30, 32, 25	wbr 2619	. . . . . . . . . . . 12 wff (abs` ((f` x) - (f` w))) < y
34	26, 33	wi 3	. . . . . . . . . . 11 wff ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y)
35	34, 17, 3	wral 1645	. . . . . . . . . 10 wff A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y)
36		crp 5300	. . . . . . . . . 10 class RR+
37	35, 23, 36	wrex 1646	. . . . . . . . 9 wff E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y)
38	37, 31, 36	wral 1645	. . . . . . . 8 wff A.y e. RR+ E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y)
39	38, 15, 3	wral 1645	. . . . . . 7 wff A.x e. a A.y e. RR+ E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y)
40	14, 39	wa 223	. . . . . 6 wff (f:a-->b /\ A.x e. a A.y e. RR+ E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))
41	40, 12	cab 1463	. . . . 5 class {f | (f:a-->b /\ A.x e. a A.y e. RR+ E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))}
42	11, 41	wceq 956	. . . 4 wff s = {f | (f:a-->b /\ A.x e. a A.y e. RR+ E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))}
43	9, 42	wa 223	. . 3 wff ((a (_ CC /\ b (_ CC) /\ s = {f | (f:a-->b /\ A.x e. a A.y e. RR+ E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))})
44	43, 2, 6, 10	copab2 3964	. 2 class {<.<.a, b>., s>. | ((a (_ CC /\ b (_ CC) /\ s = {f | (f:a-->b /\ A.x e. a A.y e. RR+ E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))})}
45	1, 44	wceq 956	1 wff -cn-> = {<.<.a, b>., s>. | ((a (_ CC /\ b (_ CC) /\ s = {f | (f:a-->b /\ A.x e. a A.y e. RR+ E.z e. RR+ A.w e. a ((abs` (x - w)) < z -> (abs` ((f` x) - (f` w))) < y))})}

This definition is referenced by:  cncfval 7264

Copyright terms: Public domain