Theorem cncff 24408

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  ∀wral 3061  ∃wrex 3070   ⊆ wss 3948   class class class wbr 5148  ⟶wf 6539  ‘cfv 6543  (class class class)co 7408  ℂcc 11107   < clt 11247   − cmin 11443  ℝ⁺crp 12973  abscabs 15180  –cn→ccncf 24391

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-cnex 11165

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-map 8821  df-cncf 24393

This theorem is referenced by:  cncfss  24414  climcncf  24415  cncfco  24422  cncfcompt2  24423  cncfmpt1f  24429  cncfmpt2ss  24431  negfcncf  24438  divcncf  24963  ivth2  24971  ivthicc  24974  evthicc2  24976  cniccbdd  24977  volivth  25123  cncombf  25174  cnmbf  25175  cniccibl  25357  cnicciblnc  25359  cnmptlimc  25406  cpnord  25451  cpnres  25453  dvrec  25471  rollelem  25505  rolle  25506  cmvth  25507  mvth  25508  dvlip  25509  c1liplem1  25512  c1lip1  25513  c1lip2  25514  dveq0  25516  dvgt0lem1  25518  dvgt0lem2  25519  dvgt0  25520  dvlt0  25521  dvge0  25522  dvle  25523  dvivthlem1  25524  dvivth  25526  dvne0  25527  dvne0f1  25528  dvcnvrelem1  25533  dvcnvrelem2  25534  dvcnvre  25535  dvcvx  25536  dvfsumle  25537  dvfsumge  25538  dvfsumabs  25539  ftc1cn  25559  ftc2  25560  ftc2ditglem  25561  ftc2ditg  25562  itgparts  25563  itgsubstlem  25564  itgsubst  25565  ulmcn  25910  psercn  25937  pserdvlem2  25939  pserdv  25940  sincn  25955  coscn  25956  logtayl  26167  dvcncxp1  26248  leibpi  26444  lgamgulmlem2  26531  ftc2re  33605  fdvposlt  33606  fdvneggt  33607  fdvposle  33608  fdvnegge  33609  gg-cmvth  35176  gg-dvfsumle  35177  ivthALT  35215  knoppcld  35376  knoppndv  35405  ftc1cnnclem  36554  ftc1cnnc  36555  ftc2nc  36565  3factsumint  40885  intlewftc  40921  dvle2  40932  cnioobibld  41953  evthiccabs  44199  cncfmptss  44293  mulc1cncfg  44295  expcnfg  44297  mulcncff  44576  cncfshift  44580  subcncff  44586  cncfcompt  44589  addcncff  44590  cncficcgt0  44594  divcncff  44597  cncfiooicclem1  44599  cncfiooiccre  44601  cncfioobd  44603  dvsubcncf  44630  dvmulcncf  44631  dvdivcncf  44633  ioodvbdlimc1lem1  44637  cnbdibl  44668  itgsubsticclem  44681  itgsubsticc  44682  itgioocnicc  44683  iblcncfioo  44684  itgiccshift  44686  itgsbtaddcnst  44688  fourierdlem18  44831  fourierdlem32  44845  fourierdlem33  44846  fourierdlem39  44852  fourierdlem48  44860  fourierdlem49  44861  fourierdlem58  44870  fourierdlem59  44871  fourierdlem71  44883  fourierdlem73  44885  fourierdlem81  44893  fourierdlem84  44896  fourierdlem85  44897  fourierdlem88  44900  fourierdlem94  44906  fourierdlem97  44909  fourierdlem101  44913  fourierdlem103  44915  fourierdlem104  44916  fourierdlem111  44923  fourierdlem112  44924  fourierdlem113  44925  fouriercn  44938