MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cncff Structured version   Unicode version

Theorem cncff 18925
Description: A continuous complex function's domain and codomain. (Contributed by Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.)
Assertion
Ref Expression
cncff  |-  ( F  e.  ( A -cn-> B )  ->  F : A
--> B )

Proof of Theorem cncff
Dummy variables  w  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cncfrss 18923 . . . 4  |-  ( F  e.  ( A -cn-> B )  ->  A  C_  CC )
2 cncfrss2 18924 . . . 4  |-  ( F  e.  ( A -cn-> B )  ->  B  C_  CC )
3 elcncf 18921 . . . 4  |-  ( ( A  C_  CC  /\  B  C_  CC )  ->  ( F  e.  ( A -cn-> B )  <->  ( 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, 2, 3syl2anc 644 . . 3  |-  ( F  e.  ( A -cn-> B )  ->  ( F  e.  ( A -cn-> B )  <-> 
( 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 ) ) ) )
54ibi 234 . 2  |-  ( F  e.  ( A -cn-> B )  ->  ( 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 ) ) )
65simpld 447 1  |-  ( F  e.  ( A -cn-> B )  ->  F : A
--> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    e. wcel 1726   A.wral 2707   E.wrex 2708    C_ wss 3322   class class class wbr 4214   -->wf 5452   ` cfv 5456  (class class class)co 6083   CCcc 8990    < clt 9122    - cmin 9293   RR+crp 10614   abscabs 12041   -cn->ccncf 18908
This theorem is referenced by:  cncfss  18931  climcncf  18932  cncfco  18939  cncfmpt1f  18945  cncfmpt2ss  18947  negfcncf  18951  ivth2  19354  ivthicc  19357  evthicc2  19359  cniccbdd  19360  volivth  19501  cncombf  19552  cnmbf  19553  cniccibl  19734  cnmptlimc  19779  cpnord  19823  cpnres  19825  dvrec  19843  rollelem  19875  rolle  19876  cmvth  19877  mvth  19878  dvlip  19879  c1liplem1  19882  c1lip1  19883  c1lip2  19884  dveq0  19886  dvgt0lem1  19888  dvgt0lem2  19889  dvgt0  19890  dvlt0  19891  dvge0  19892  dvle  19893  dvivthlem1  19894  dvivth  19896  dvne0  19897  dvne0f1  19898  dvcnvrelem1  19903  dvcnvrelem2  19904  dvcnvre  19905  dvcvx  19906  dvfsumle  19907  dvfsumge  19908  dvfsumabs  19909  ftc1cn  19929  ftc2  19930  ftc2ditglem  19931  ftc2ditg  19932  itgparts  19933  itgsubstlem  19934  itgsubst  19935  ulmcn  20317  psercn  20344  pserdvlem2  20346  pserdv  20347  sincn  20362  coscn  20363  logtayl  20553  leibpi  20784  lgamgulmlem2  24816  cnicciblnc  26278  ftc1cnnclem  26280  ftc1cnnc  26281  ftc2nc  26291  ivthALT  26340  cncfmptss  27695  mulc1cncfg  27699  expcnfg  27704
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703  ax-cnex 9048
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-opab 4269  df-id 4500  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-fv 5464  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-map 7022  df-cncf 18910
  Copyright terms: Public domain W3C validator