Definition df-cncf 18861

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

Assertion

Ref	Expression
df-cncf	|- -cn-> = ( a e. ~P CC , b e. ~P CC |-> { f e. ( b ^m a ) | A. x e. a A. e e. RR+ E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e ) } )

Distinct variable group:   a, b, d, e, f, x, y

Detailed syntax breakdown of Definition df-cncf

Step	Hyp	Ref	Expression
1		ccncf 18859	. 2 class -cn->
2		va	. . 3 set a
3		vb	. . 3 set b
4		cc 8944	. . . 4 class CC
5	4	cpw 3759	. . 3 class ~P CC
6		vx	. . . . . . . . . . . . 13 set x
7	6	cv 1648	. . . . . . . . . . . 12 class x
8		vy	. . . . . . . . . . . . 13 set y
9	8	cv 1648	. . . . . . . . . . . 12 class y
10		cmin 9247	. . . . . . . . . . . 12 class -
11	7, 9, 10	co 6040	. . . . . . . . . . 11 class ( x - y )
12		cabs 11994	. . . . . . . . . . 11 class abs
13	11, 12	cfv 5413	. . . . . . . . . 10 class ( abs ` ( x - y ) )
14		vd	. . . . . . . . . . 11 set d
15	14	cv 1648	. . . . . . . . . 10 class d
16		clt 9076	. . . . . . . . . 10 class <
17	13, 15, 16	wbr 4172	. . . . . . . . 9 wff ( abs ` ( x - y ) ) < d
18		vf	. . . . . . . . . . . . . 14 set f
19	18	cv 1648	. . . . . . . . . . . . 13 class f
20	7, 19	cfv 5413	. . . . . . . . . . . 12 class ( f ` x )
21	9, 19	cfv 5413	. . . . . . . . . . . 12 class ( f ` y )
22	20, 21, 10	co 6040	. . . . . . . . . . 11 class ( ( f ` x ) - ( f ` y ) )
23	22, 12	cfv 5413	. . . . . . . . . 10 class ( abs ` ( ( f ` x ) - ( f ` y ) ) )
24		ve	. . . . . . . . . . 11 set e
25	24	cv 1648	. . . . . . . . . 10 class e
26	23, 25, 16	wbr 4172	. . . . . . . . 9 wff ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e
27	17, 26	wi 4	. . . . . . . 8 wff ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e )
28	2	cv 1648	. . . . . . . 8 class a
29	27, 8, 28	wral 2666	. . . . . . 7 wff A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e )
30		crp 10568	. . . . . . 7 class RR+
31	29, 14, 30	wrex 2667	. . . . . 6 wff E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e )
32	31, 24, 30	wral 2666	. . . . 5 wff A. e e. RR+ E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e )
33	32, 6, 28	wral 2666	. . . 4 wff A. x e. a A. e e. RR+ E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e )
34	3	cv 1648	. . . . 5 class b
35		cmap 6977	. . . . 5 class ^m
36	34, 28, 35	co 6040	. . . 4 class ( b ^m a )
37	33, 18, 36	crab 2670	. . 3 class { f e. ( b ^m a ) | A. x e. a A. e e. RR+ E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e ) }
38	2, 3, 5, 5, 37	cmpt2 6042	. 2 class ( a e. ~P CC , b e. ~P CC |-> { f e. ( b ^m a ) | A. x e. a A. e e. RR+ E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e ) } )
39	1, 38	wceq 1649	1 wff -cn-> = ( a e. ~P CC , b e. ~P CC |-> { f e. ( b ^m a ) | A. x e. a A. e e. RR+ E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e ) } )

This definition is referenced by:  cncfval  18871  cncfrss  18874  cncfrss2  18875