MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cncf Unicode version

Definition df-cncf 18382
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
StepHypRef Expression
1 ccncf 18380 . 2  class  -cn->
2 va . . 3  set  a
3 vb . . 3  set  b
4 cc 8735 . . . 4  class  CC
54cpw 3625 . . 3  class  ~P CC
6 vx . . . . . . . . . . . . 13  set  x
76cv 1622 . . . . . . . . . . . 12  class  x
8 vy . . . . . . . . . . . . 13  set  y
98cv 1622 . . . . . . . . . . . 12  class  y
10 cmin 9037 . . . . . . . . . . . 12  class  -
117, 9, 10co 5858 . . . . . . . . . . 11  class  ( x  -  y )
12 cabs 11719 . . . . . . . . . . 11  class  abs
1311, 12cfv 5255 . . . . . . . . . 10  class  ( abs `  ( x  -  y
) )
14 vd . . . . . . . . . . 11  set  d
1514cv 1622 . . . . . . . . . 10  class  d
16 clt 8867 . . . . . . . . . 10  class  <
1713, 15, 16wbr 4023 . . . . . . . . 9  wff  ( abs `  ( x  -  y
) )  <  d
18 vf . . . . . . . . . . . . . 14  set  f
1918cv 1622 . . . . . . . . . . . . 13  class  f
207, 19cfv 5255 . . . . . . . . . . . 12  class  ( f `
 x )
219, 19cfv 5255 . . . . . . . . . . . 12  class  ( f `
 y )
2220, 21, 10co 5858 . . . . . . . . . . 11  class  ( ( f `  x )  -  ( f `  y ) )
2322, 12cfv 5255 . . . . . . . . . 10  class  ( abs `  ( ( f `  x )  -  (
f `  y )
) )
24 ve . . . . . . . . . . 11  set  e
2524cv 1622 . . . . . . . . . 10  class  e
2623, 25, 16wbr 4023 . . . . . . . . 9  wff  ( abs `  ( ( f `  x )  -  (
f `  y )
) )  <  e
2717, 26wi 4 . . . . . . . 8  wff  ( ( abs `  ( x  -  y ) )  <  d  ->  ( abs `  ( ( f `
 x )  -  ( f `  y
) ) )  < 
e )
282cv 1622 . . . . . . . 8  class  a
2927, 8, 28wral 2543 . . . . . . 7  wff  A. y  e.  a  ( ( abs `  ( x  -  y ) )  < 
d  ->  ( abs `  ( ( f `  x )  -  (
f `  y )
) )  <  e
)
30 crp 10354 . . . . . . 7  class  RR+
3129, 14, 30wrex 2544 . . . . . 6  wff  E. d  e.  RR+  A. y  e.  a  ( ( abs `  ( x  -  y
) )  <  d  ->  ( abs `  (
( f `  x
)  -  ( f `
 y ) ) )  <  e )
3231, 24, 30wral 2543 . . . . 5  wff  A. e  e.  RR+  E. d  e.  RR+  A. y  e.  a  ( ( abs `  (
x  -  y ) )  <  d  -> 
( abs `  (
( f `  x
)  -  ( f `
 y ) ) )  <  e )
3332, 6, 28wral 2543 . . . 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 )
343cv 1622 . . . . 5  class  b
35 cmap 6772 . . . . 5  class  ^m
3634, 28, 35co 5858 . . . 4  class  ( b  ^m  a )
3733, 18, 36crab 2547 . . 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 ) }
382, 3, 5, 5, 37cmpt2 5860 . 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 ) } )
391, 38wceq 1623 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 ) } )
Colors of variables: wff set class
This definition is referenced by:  cncfval  18392  cncfrss  18395  cncfrss2  18396
  Copyright terms: Public domain W3C validator