Theorem cncff 24860

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 24858	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
2		cncfrss2 24859	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
3		elcncf 24856	. . . 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 3890   class class class wbr 5086  ⟶wf 6495  ‘cfv 6499  (class class class)co 7367  ℂcc 11036   < clt 11179   − cmin 11377  ℝ⁺crp 12942  abscabs 15196  –cn→ccncf 24843

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 5232  ax-nul 5242  ax-pow 5308  ax-pr 5376  ax-un 7689  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 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6455  df-fun 6501  df-fn 6502  df-f 6503  df-fv 6507  df-ov 7370  df-oprab 7371  df-mpo 7372  df-map 8775  df-cncf 24845

This theorem is referenced by:  cncfss  24866  climcncf  24867  cncfco  24874  cncfcompt2  24875  cncfmpt1f  24881  cncfmpt2ss  24883  negfcncf  24890  divcncf  25414  ivth2  25422  ivthicc  25425  evthicc2  25427  cniccbdd  25428  volivth  25574  cncombf  25625  cnmbf  25626  cniccibl  25808  cnicciblnc  25810  cnmptlimc  25857  cpnord  25902  cpnres  25904  dvrec  25922  rollelem  25956  rolle  25957  cmvth  25958  mvth  25959  dvlip  25960  c1liplem1  25963  c1lip1  25964  c1lip2  25965  dveq0  25967  dvgt0lem1  25969  dvgt0lem2  25970  dvgt0  25971  dvlt0  25972  dvge0  25973  dvle  25974  dvivthlem1  25975  dvivth  25977  dvne0  25978  dvne0f1  25979  dvcnvrelem1  25984  dvcnvrelem2  25985  dvcnvre  25986  dvcvx  25987  dvfsumle  25988  dvfsumge  25989  dvfsumabs  25990  ftc1cn  26010  ftc2  26011  ftc2ditglem  26012  ftc2ditg  26013  itgparts  26014  itgsubstlem  26015  itgsubst  26016  ulmcn  26364  psercn  26391  pserdvlem2  26393  pserdv  26394  sincn  26409  coscn  26410  logtayl  26624  dvcncxp1  26707  leibpi  26906  lgamgulmlem2  26993  ftc2re  34742  fdvposlt  34743  fdvneggt  34744  fdvposle  34745  fdvnegge  34746  ivthALT  36517  knoppcld  36765  knoppndv  36794  ftc1cnnclem  38012  ftc1cnnc  38013  ftc2nc  38023  3factsumint  42464  intlewftc  42500  dvle2  42511  cnioobibld  43642  evthiccabs  45926  cncfmptss  46017  mulc1cncfg  46019  expcnfg  46021  mulcncff  46298  cncfshift  46302  subcncff  46308  cncfcompt  46311  addcncff  46312  cncficcgt0  46316  divcncff  46319  cncfiooicclem1  46321  cncfiooiccre  46323  cncfioobd  46325  dvsubcncf  46352  dvmulcncf  46353  dvdivcncf  46355  ioodvbdlimc1lem1  46359  cnbdibl  46390  itgsubsticclem  46403  itgsubsticc  46404  itgioocnicc  46405  iblcncfioo  46406  itgiccshift  46408  itgsbtaddcnst  46410  fourierdlem18  46553  fourierdlem32  46567  fourierdlem33  46568  fourierdlem39  46574  fourierdlem48  46582  fourierdlem49  46583  fourierdlem58  46592  fourierdlem59  46593  fourierdlem71  46605  fourierdlem73  46607  fourierdlem81  46615  fourierdlem84  46618  fourierdlem85  46619  fourierdlem88  46622  fourierdlem94  46628  fourierdlem97  46631  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem112  46646  fourierdlem113  46647  fouriercn  46660