Definition df-cncf 13725

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 13724	. 2 class -cn->
2		va	. . 3 setvar a
3		vb	. . 3 setvar b
4		cc 7800	. . . 4 class CC
5	4	cpw 3574	. . 3 class ~P CC
6		vx	. . . . . . . . . . . . 13 setvar x
7	6	cv 1352	. . . . . . . . . . . 12 class x
8		vy	. . . . . . . . . . . . 13 setvar y
9	8	cv 1352	. . . . . . . . . . . 12 class y
10		cmin 8118	. . . . . . . . . . . 12 class -
11	7, 9, 10	co 5869	. . . . . . . . . . 11 class ( x - y )
12		cabs 10990	. . . . . . . . . . 11 class abs
13	11, 12	cfv 5212	. . . . . . . . . 10 class ( abs ` ( x - y ) )
14		vd	. . . . . . . . . . 11 setvar d
15	14	cv 1352	. . . . . . . . . 10 class d
16		clt 7982	. . . . . . . . . 10 class <
17	13, 15, 16	wbr 4000	. . . . . . . . 9 wff ( abs ` ( x - y ) ) < d
18		vf	. . . . . . . . . . . . . 14 setvar f
19	18	cv 1352	. . . . . . . . . . . . 13 class f
20	7, 19	cfv 5212	. . . . . . . . . . . 12 class ( f ` x )
21	9, 19	cfv 5212	. . . . . . . . . . . 12 class ( f ` y )
22	20, 21, 10	co 5869	. . . . . . . . . . 11 class ( ( f ` x ) - ( f ` y ) )
23	22, 12	cfv 5212	. . . . . . . . . 10 class ( abs ` ( ( f ` x ) - ( f ` y ) ) )
24		ve	. . . . . . . . . . 11 setvar e
25	24	cv 1352	. . . . . . . . . 10 class e
26	23, 25, 16	wbr 4000	. . . . . . . . 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 1352	. . . . . . . 8 class a
29	27, 8, 28	wral 2455	. . . . . . 7 wff A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e )
30		crp 9640	. . . . . . 7 class RR+
31	29, 14, 30	wrex 2456	. . . . . 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 2455	. . . . 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 2455	. . . 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 1352	. . . . 5 class b
35		cmap 6642	. . . . 5 class ^m
36	34, 28, 35	co 5869	. . . 4 class ( b ^m a )
37	33, 18, 36	crab 2459	. . 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	cmpo 5871	. 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 1353	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  13726  cncfrss  13729  cncfrss2  13730