Theorem cncff 24846

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 24844	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
2		cncfrss2 24845	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
3		elcncf 24842	. . . 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 3061   ⊆ wss 3902   class class class wbr 5099  ⟶wf 6489  ‘cfv 6493  (class class class)co 7360  ℂcc 11028   < clt 11170   − cmin 11368  ℝ⁺crp 12909  abscabs 15161  –cn→ccncf 24829

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 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-cnex 11086

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 3062  df-rab 3401  df-v 3443  df-sbc 3742  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7363  df-oprab 7364  df-mpo 7365  df-map 8769  df-cncf 24831

This theorem is referenced by:  cncfss  24852  climcncf  24853  cncfco  24860  cncfcompt2  24861  cncfmpt1f  24867  cncfmpt2ss  24869  negfcncf  24877  divcncf  25408  ivth2  25416  ivthicc  25419  evthicc2  25421  cniccbdd  25422  volivth  25568  cncombf  25619  cnmbf  25620  cniccibl  25802  cnicciblnc  25804  cnmptlimc  25851  cpnord  25897  cpnres  25899  dvrec  25919  rollelem  25953  rolle  25954  cmvth  25955  cmvthOLD  25956  mvth  25957  dvlip  25958  c1liplem1  25961  c1lip1  25962  c1lip2  25963  dveq0  25965  dvgt0lem1  25967  dvgt0lem2  25968  dvgt0  25969  dvlt0  25970  dvge0  25971  dvle  25972  dvivthlem1  25973  dvivth  25975  dvne0  25976  dvne0f1  25977  dvcnvrelem1  25982  dvcnvrelem2  25983  dvcnvre  25984  dvcvx  25985  dvfsumle  25986  dvfsumleOLD  25987  dvfsumge  25988  dvfsumabs  25989  ftc1cn  26010  ftc2  26011  ftc2ditglem  26012  ftc2ditg  26013  itgparts  26014  itgsubstlem  26015  itgsubst  26016  ulmcn  26368  psercn  26396  pserdvlem2  26398  pserdv  26399  sincn  26414  coscn  26415  logtayl  26629  dvcncxp1  26712  leibpi  26912  lgamgulmlem2  27000  ftc2re  34736  fdvposlt  34737  fdvneggt  34738  fdvposle  34739  fdvnegge  34740  ivthALT  36510  knoppcld  36680  knoppndv  36709  ftc1cnnclem  37863  ftc1cnnc  37864  ftc2nc  37874  3factsumint  42316  intlewftc  42352  dvle2  42363  cnioobibld  43492  evthiccabs  45778  cncfmptss  45869  mulc1cncfg  45871  expcnfg  45873  mulcncff  46150  cncfshift  46154  subcncff  46160  cncfcompt  46163  addcncff  46164  cncficcgt0  46168  divcncff  46171  cncfiooicclem1  46173  cncfiooiccre  46175  cncfioobd  46177  dvsubcncf  46204  dvmulcncf  46205  dvdivcncf  46207  ioodvbdlimc1lem1  46211  cnbdibl  46242  itgsubsticclem  46255  itgsubsticc  46256  itgioocnicc  46257  iblcncfioo  46258  itgiccshift  46260  itgsbtaddcnst  46262  fourierdlem18  46405  fourierdlem32  46419  fourierdlem33  46420  fourierdlem39  46426  fourierdlem48  46434  fourierdlem49  46435  fourierdlem58  46444  fourierdlem59  46445  fourierdlem71  46457  fourierdlem73  46459  fourierdlem81  46467  fourierdlem84  46470  fourierdlem85  46471  fourierdlem88  46474  fourierdlem94  46480  fourierdlem97  46483  fourierdlem101  46487  fourierdlem103  46489  fourierdlem104  46490  fourierdlem111  46497  fourierdlem112  46498  fourierdlem113  46499  fouriercn  46512