Theorem cncff 24932

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2105  ∀wral 3058  ∃wrex 3067   ⊆ wss 3962   class class class wbr 5147  ⟶wf 6558  ‘cfv 6562  (class class class)co 7430  ℂcc 11150   < clt 11292   − cmin 11489  ℝ⁺crp 13031  abscabs 15269  –cn→ccncf 24915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-map 8866  df-cncf 24917

This theorem is referenced by:  cncfss  24938  climcncf  24939  cncfco  24946  cncfcompt2  24947  cncfmpt1f  24953  cncfmpt2ss  24955  negfcncf  24963  divcncf  25495  ivth2  25503  ivthicc  25506  evthicc2  25508  cniccbdd  25509  volivth  25655  cncombf  25706  cnmbf  25707  cniccibl  25890  cnicciblnc  25892  cnmptlimc  25939  cpnord  25985  cpnres  25987  dvrec  26007  rollelem  26041  rolle  26042  cmvth  26043  cmvthOLD  26044  mvth  26045  dvlip  26046  c1liplem1  26049  c1lip1  26050  c1lip2  26051  dveq0  26053  dvgt0lem1  26055  dvgt0lem2  26056  dvgt0  26057  dvlt0  26058  dvge0  26059  dvle  26060  dvivthlem1  26061  dvivth  26063  dvne0  26064  dvne0f1  26065  dvcnvrelem1  26070  dvcnvrelem2  26071  dvcnvre  26072  dvcvx  26073  dvfsumle  26074  dvfsumleOLD  26075  dvfsumge  26076  dvfsumabs  26077  ftc1cn  26098  ftc2  26099  ftc2ditglem  26100  ftc2ditg  26101  itgparts  26102  itgsubstlem  26103  itgsubst  26104  ulmcn  26456  psercn  26484  pserdvlem2  26486  pserdv  26487  sincn  26502  coscn  26503  logtayl  26716  dvcncxp1  26799  leibpi  26999  lgamgulmlem2  27087  ftc2re  34591  fdvposlt  34592  fdvneggt  34593  fdvposle  34594  fdvnegge  34595  ivthALT  36317  knoppcld  36487  knoppndv  36516  ftc1cnnclem  37677  ftc1cnnc  37678  ftc2nc  37688  3factsumint  42006  intlewftc  42042  dvle2  42053  cnioobibld  43202  evthiccabs  45448  cncfmptss  45542  mulc1cncfg  45544  expcnfg  45546  mulcncff  45825  cncfshift  45829  subcncff  45835  cncfcompt  45838  addcncff  45839  cncficcgt0  45843  divcncff  45846  cncfiooicclem1  45848  cncfiooiccre  45850  cncfioobd  45852  dvsubcncf  45879  dvmulcncf  45880  dvdivcncf  45882  ioodvbdlimc1lem1  45886  cnbdibl  45917  itgsubsticclem  45930  itgsubsticc  45931  itgioocnicc  45932  iblcncfioo  45933  itgiccshift  45935  itgsbtaddcnst  45937  fourierdlem18  46080  fourierdlem32  46094  fourierdlem33  46095  fourierdlem39  46101  fourierdlem48  46109  fourierdlem49  46110  fourierdlem58  46119  fourierdlem59  46120  fourierdlem71  46132  fourierdlem73  46134  fourierdlem81  46142  fourierdlem84  46145  fourierdlem85  46146  fourierdlem88  46149  fourierdlem94  46155  fourierdlem97  46158  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fourierdlem112  46173  fourierdlem113  46174  fouriercn  46187