Theorem cncff 24854

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 24852	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
2		cncfrss2 24853	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
3		elcncf 24850	. . . 4 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))))
4	1, 2, 3	syl2anc 585	. . 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 2114  ∀wral 3052  ∃wrex 3062   ⊆ wss 3903   class class class wbr 5100  ⟶wf 6496  ‘cfv 6500  (class class class)co 7368  ℂcc 11036   < clt 11178   − cmin 11376  ℝ⁺crp 12917  abscabs 15169  –cn→ccncf 24837

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-map 8777  df-cncf 24839

This theorem is referenced by:  cncfss  24860  climcncf  24861  cncfco  24868  cncfcompt2  24869  cncfmpt1f  24875  cncfmpt2ss  24877  negfcncf  24885  divcncf  25416  ivth2  25424  ivthicc  25427  evthicc2  25429  cniccbdd  25430  volivth  25576  cncombf  25627  cnmbf  25628  cniccibl  25810  cnicciblnc  25812  cnmptlimc  25859  cpnord  25905  cpnres  25907  dvrec  25927  rollelem  25961  rolle  25962  cmvth  25963  cmvthOLD  25964  mvth  25965  dvlip  25966  c1liplem1  25969  c1lip1  25970  c1lip2  25971  dveq0  25973  dvgt0lem1  25975  dvgt0lem2  25976  dvgt0  25977  dvlt0  25978  dvge0  25979  dvle  25980  dvivthlem1  25981  dvivth  25983  dvne0  25984  dvne0f1  25985  dvcnvrelem1  25990  dvcnvrelem2  25991  dvcnvre  25992  dvcvx  25993  dvfsumle  25994  dvfsumleOLD  25995  dvfsumge  25996  dvfsumabs  25997  ftc1cn  26018  ftc2  26019  ftc2ditglem  26020  ftc2ditg  26021  itgparts  26022  itgsubstlem  26023  itgsubst  26024  ulmcn  26376  psercn  26404  pserdvlem2  26406  pserdv  26407  sincn  26422  coscn  26423  logtayl  26637  dvcncxp1  26720  leibpi  26920  lgamgulmlem2  27008  ftc2re  34775  fdvposlt  34776  fdvneggt  34777  fdvposle  34778  fdvnegge  34779  ivthALT  36548  knoppcld  36724  knoppndv  36753  ftc1cnnclem  37931  ftc1cnnc  37932  ftc2nc  37942  3factsumint  42384  intlewftc  42420  dvle2  42431  cnioobibld  43560  evthiccabs  45845  cncfmptss  45936  mulc1cncfg  45938  expcnfg  45940  mulcncff  46217  cncfshift  46221  subcncff  46227  cncfcompt  46230  addcncff  46231  cncficcgt0  46235  divcncff  46238  cncfiooicclem1  46240  cncfiooiccre  46242  cncfioobd  46244  dvsubcncf  46271  dvmulcncf  46272  dvdivcncf  46274  ioodvbdlimc1lem1  46278  cnbdibl  46309  itgsubsticclem  46322  itgsubsticc  46323  itgioocnicc  46324  iblcncfioo  46325  itgiccshift  46327  itgsbtaddcnst  46329  fourierdlem18  46472  fourierdlem32  46486  fourierdlem33  46487  fourierdlem39  46493  fourierdlem48  46501  fourierdlem49  46502  fourierdlem58  46511  fourierdlem59  46512  fourierdlem71  46524  fourierdlem73  46526  fourierdlem81  46534  fourierdlem84  46537  fourierdlem85  46538  fourierdlem88  46541  fourierdlem94  46547  fourierdlem97  46550  fourierdlem101  46554  fourierdlem103  46556  fourierdlem104  46557  fourierdlem111  46564  fourierdlem112  46565  fourierdlem113  46566  fouriercn  46579