Theorem cncff 23962

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 23960	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
2		cncfrss2 23961	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
3		elcncf 23958	. . . 4 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))))
4	1, 2, 3	syl2anc 583	. . 3 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))))
5	4	ibi 266	. 2 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))
6	5	simpld 494	1 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064   ⊆ wss 3883   class class class wbr 5070  ⟶wf 6414  ‘cfv 6418  (class class class)co 7255  ℂcc 10800   < clt 10940   − cmin 11135  ℝ⁺crp 12659  abscabs 14873  –cn→ccncf 23945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-map 8575  df-cncf 23947

This theorem is referenced by:  cncfss  23968  climcncf  23969  cncfco  23976  cncfcompt2  23977  cncfmpt1f  23983  cncfmpt2ss  23985  negfcncf  23992  divcncf  24516  ivth2  24524  ivthicc  24527  evthicc2  24529  cniccbdd  24530  volivth  24676  cncombf  24727  cnmbf  24728  cniccibl  24910  cnicciblnc  24912  cnmptlimc  24959  cpnord  25004  cpnres  25006  dvrec  25024  rollelem  25058  rolle  25059  cmvth  25060  mvth  25061  dvlip  25062  c1liplem1  25065  c1lip1  25066  c1lip2  25067  dveq0  25069  dvgt0lem1  25071  dvgt0lem2  25072  dvgt0  25073  dvlt0  25074  dvge0  25075  dvle  25076  dvivthlem1  25077  dvivth  25079  dvne0  25080  dvne0f1  25081  dvcnvrelem1  25086  dvcnvrelem2  25087  dvcnvre  25088  dvcvx  25089  dvfsumle  25090  dvfsumge  25091  dvfsumabs  25092  ftc1cn  25112  ftc2  25113  ftc2ditglem  25114  ftc2ditg  25115  itgparts  25116  itgsubstlem  25117  itgsubst  25118  ulmcn  25463  psercn  25490  pserdvlem2  25492  pserdv  25493  sincn  25508  coscn  25509  logtayl  25720  dvcncxp1  25801  leibpi  25997  lgamgulmlem2  26084  ftc2re  32478  fdvposlt  32479  fdvneggt  32480  fdvposle  32481  fdvnegge  32482  ivthALT  34451  knoppcld  34612  knoppndv  34641  ftc1cnnclem  35775  ftc1cnnc  35776  ftc2nc  35786  3factsumint  39961  intlewftc  39997  dvle2  40008  cnioobibld  40961  evthiccabs  42924  cncfmptss  43018  mulc1cncfg  43020  expcnfg  43022  mulcncff  43301  cncfshift  43305  subcncff  43311  cncfcompt  43314  addcncff  43315  cncficcgt0  43319  divcncff  43322  cncfiooicclem1  43324  cncfiooiccre  43326  cncfioobd  43328  dvsubcncf  43355  dvmulcncf  43356  dvdivcncf  43358  ioodvbdlimc1lem1  43362  cnbdibl  43393  itgsubsticclem  43406  itgsubsticc  43407  itgioocnicc  43408  iblcncfioo  43409  itgiccshift  43411  itgsbtaddcnst  43413  fourierdlem18  43556  fourierdlem32  43570  fourierdlem33  43571  fourierdlem39  43577  fourierdlem48  43585  fourierdlem49  43586  fourierdlem58  43595  fourierdlem59  43596  fourierdlem71  43608  fourierdlem73  43610  fourierdlem81  43618  fourierdlem84  43621  fourierdlem85  43622  fourierdlem88  43625  fourierdlem94  43631  fourierdlem97  43634  fourierdlem101  43638  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fourierdlem112  43649  fourierdlem113  43650  fouriercn  43663