Theorem cncff 24065

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	⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐹:𝐴⟶𝐵)

Proof of Theorem cncff

Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cncfrss 24063	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
2		cncfrss2 24064	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
3		elcncf 24061	. . . 4 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))))
4	1, 2, 3	syl2anc 584	. . 3 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))))
5	4	ibi 266	. 2 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))
6	5	simpld 495	1 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2107  ∀wral 3065  ∃wrex 3066   ⊆ wss 3888   class class class wbr 5075  ⟶wf 6433  ‘cfv 6437  (class class class)co 7284  ℂcc 10878   < clt 11018   − cmin 11214  ℝ⁺crp 12739  abscabs 14954  –cn→ccncf 24048

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-cnex 10936

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-fv 6445  df-ov 7287  df-oprab 7288  df-mpo 7289  df-map 8626  df-cncf 24050

This theorem is referenced by:  cncfss  24071  climcncf  24072  cncfco  24079  cncfcompt2  24080  cncfmpt1f  24086  cncfmpt2ss  24088  negfcncf  24095  divcncf  24620  ivth2  24628  ivthicc  24631  evthicc2  24633  cniccbdd  24634  volivth  24780  cncombf  24831  cnmbf  24832  cniccibl  25014  cnicciblnc  25016  cnmptlimc  25063  cpnord  25108  cpnres  25110  dvrec  25128  rollelem  25162  rolle  25163  cmvth  25164  mvth  25165  dvlip  25166  c1liplem1  25169  c1lip1  25170  c1lip2  25171  dveq0  25173  dvgt0lem1  25175  dvgt0lem2  25176  dvgt0  25177  dvlt0  25178  dvge0  25179  dvle  25180  dvivthlem1  25181  dvivth  25183  dvne0  25184  dvne0f1  25185  dvcnvrelem1  25190  dvcnvrelem2  25191  dvcnvre  25192  dvcvx  25193  dvfsumle  25194  dvfsumge  25195  dvfsumabs  25196  ftc1cn  25216  ftc2  25217  ftc2ditglem  25218  ftc2ditg  25219  itgparts  25220  itgsubstlem  25221  itgsubst  25222  ulmcn  25567  psercn  25594  pserdvlem2  25596  pserdv  25597  sincn  25612  coscn  25613  logtayl  25824  dvcncxp1  25905  leibpi  26101  lgamgulmlem2  26188  ftc2re  32587  fdvposlt  32588  fdvneggt  32589  fdvposle  32590  fdvnegge  32591  ivthALT  34533  knoppcld  34694  knoppndv  34723  ftc1cnnclem  35857  ftc1cnnc  35858  ftc2nc  35868  3factsumint  40040  intlewftc  40076  dvle2  40087  cnioobibld  41052  evthiccabs  43041  cncfmptss  43135  mulc1cncfg  43137  expcnfg  43139  mulcncff  43418  cncfshift  43422  subcncff  43428  cncfcompt  43431  addcncff  43432  cncficcgt0  43436  divcncff  43439  cncfiooicclem1  43441  cncfiooiccre  43443  cncfioobd  43445  dvsubcncf  43472  dvmulcncf  43473  dvdivcncf  43475  ioodvbdlimc1lem1  43479  cnbdibl  43510  itgsubsticclem  43523  itgsubsticc  43524  itgioocnicc  43525  iblcncfioo  43526  itgiccshift  43528  itgsbtaddcnst  43530  fourierdlem18  43673  fourierdlem32  43687  fourierdlem33  43688  fourierdlem39  43694  fourierdlem48  43702  fourierdlem49  43703  fourierdlem58  43712  fourierdlem59  43713  fourierdlem71  43725  fourierdlem73  43727  fourierdlem81  43735  fourierdlem84  43738  fourierdlem85  43739  fourierdlem88  43742  fourierdlem94  43748  fourierdlem97  43751  fourierdlem101  43755  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  fourierdlem112  43766  fourierdlem113  43767  fouriercn  43780