Theorem cncff 24938

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 24936	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
2		cncfrss2 24937	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
3		elcncf 24934	. . . 4 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))))
4	1, 2, 3	syl2anc 583	. . 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 2108  ∀wral 3067  ∃wrex 3076   ⊆ wss 3976   class class class wbr 5166  ⟶wf 6569  ‘cfv 6573  (class class class)co 7448  ℂcc 11182   < clt 11324   − cmin 11520  ℝ⁺crp 13057  abscabs 15283  –cn→ccncf 24921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-map 8886  df-cncf 24923

This theorem is referenced by:  cncfss  24944  climcncf  24945  cncfco  24952  cncfcompt2  24953  cncfmpt1f  24959  cncfmpt2ss  24961  negfcncf  24969  divcncf  25501  ivth2  25509  ivthicc  25512  evthicc2  25514  cniccbdd  25515  volivth  25661  cncombf  25712  cnmbf  25713  cniccibl  25896  cnicciblnc  25898  cnmptlimc  25945  cpnord  25991  cpnres  25993  dvrec  26013  rollelem  26047  rolle  26048  cmvth  26049  cmvthOLD  26050  mvth  26051  dvlip  26052  c1liplem1  26055  c1lip1  26056  c1lip2  26057  dveq0  26059  dvgt0lem1  26061  dvgt0lem2  26062  dvgt0  26063  dvlt0  26064  dvge0  26065  dvle  26066  dvivthlem1  26067  dvivth  26069  dvne0  26070  dvne0f1  26071  dvcnvrelem1  26076  dvcnvrelem2  26077  dvcnvre  26078  dvcvx  26079  dvfsumle  26080  dvfsumleOLD  26081  dvfsumge  26082  dvfsumabs  26083  ftc1cn  26104  ftc2  26105  ftc2ditglem  26106  ftc2ditg  26107  itgparts  26108  itgsubstlem  26109  itgsubst  26110  ulmcn  26460  psercn  26488  pserdvlem2  26490  pserdv  26491  sincn  26506  coscn  26507  logtayl  26720  dvcncxp1  26803  leibpi  27003  lgamgulmlem2  27091  ftc2re  34575  fdvposlt  34576  fdvneggt  34577  fdvposle  34578  fdvnegge  34579  ivthALT  36301  knoppcld  36471  knoppndv  36500  ftc1cnnclem  37651  ftc1cnnc  37652  ftc2nc  37662  3factsumint  41982  intlewftc  42018  dvle2  42029  cnioobibld  43175  evthiccabs  45414  cncfmptss  45508  mulc1cncfg  45510  expcnfg  45512  mulcncff  45791  cncfshift  45795  subcncff  45801  cncfcompt  45804  addcncff  45805  cncficcgt0  45809  divcncff  45812  cncfiooicclem1  45814  cncfiooiccre  45816  cncfioobd  45818  dvsubcncf  45845  dvmulcncf  45846  dvdivcncf  45848  ioodvbdlimc1lem1  45852  cnbdibl  45883  itgsubsticclem  45896  itgsubsticc  45897  itgioocnicc  45898  iblcncfioo  45899  itgiccshift  45901  itgsbtaddcnst  45903  fourierdlem18  46046  fourierdlem32  46060  fourierdlem33  46061  fourierdlem39  46067  fourierdlem48  46075  fourierdlem49  46076  fourierdlem58  46085  fourierdlem59  46086  fourierdlem71  46098  fourierdlem73  46100  fourierdlem81  46108  fourierdlem84  46111  fourierdlem85  46112  fourierdlem88  46115  fourierdlem94  46121  fourierdlem97  46124  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fourierdlem112  46139  fourierdlem113  46140  fouriercn  46153