Theorem cncff 24823

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 24821	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
2		cncfrss2 24822	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
3		elcncf 24819	. . . 4 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))))
4	1, 2, 3	syl2anc 584	. . 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 2113  ∀wral 3049  ∃wrex 3058   ⊆ wss 3899   class class class wbr 5095  ⟶wf 6485  ‘cfv 6489  (class class class)co 7355  ℂcc 11014   < clt 11156   − cmin 11354  ℝ⁺crp 12900  abscabs 15151  –cn→ccncf 24806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-cnex 11072

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-fv 6497  df-ov 7358  df-oprab 7359  df-mpo 7360  df-map 8761  df-cncf 24808

This theorem is referenced by:  cncfss  24829  climcncf  24830  cncfco  24837  cncfcompt2  24838  cncfmpt1f  24844  cncfmpt2ss  24846  negfcncf  24854  divcncf  25385  ivth2  25393  ivthicc  25396  evthicc2  25398  cniccbdd  25399  volivth  25545  cncombf  25596  cnmbf  25597  cniccibl  25779  cnicciblnc  25781  cnmptlimc  25828  cpnord  25874  cpnres  25876  dvrec  25896  rollelem  25930  rolle  25931  cmvth  25932  cmvthOLD  25933  mvth  25934  dvlip  25935  c1liplem1  25938  c1lip1  25939  c1lip2  25940  dveq0  25942  dvgt0lem1  25944  dvgt0lem2  25945  dvgt0  25946  dvlt0  25947  dvge0  25948  dvle  25949  dvivthlem1  25950  dvivth  25952  dvne0  25953  dvne0f1  25954  dvcnvrelem1  25959  dvcnvrelem2  25960  dvcnvre  25961  dvcvx  25962  dvfsumle  25963  dvfsumleOLD  25964  dvfsumge  25965  dvfsumabs  25966  ftc1cn  25987  ftc2  25988  ftc2ditglem  25989  ftc2ditg  25990  itgparts  25991  itgsubstlem  25992  itgsubst  25993  ulmcn  26345  psercn  26373  pserdvlem2  26375  pserdv  26376  sincn  26391  coscn  26392  logtayl  26606  dvcncxp1  26689  leibpi  26889  lgamgulmlem2  26977  ftc2re  34622  fdvposlt  34623  fdvneggt  34624  fdvposle  34625  fdvnegge  34626  ivthALT  36390  knoppcld  36560  knoppndv  36589  ftc1cnnclem  37741  ftc1cnnc  37742  ftc2nc  37752  3factsumint  42128  intlewftc  42164  dvle2  42175  cnioobibld  43321  evthiccabs  45610  cncfmptss  45701  mulc1cncfg  45703  expcnfg  45705  mulcncff  45982  cncfshift  45986  subcncff  45992  cncfcompt  45995  addcncff  45996  cncficcgt0  46000  divcncff  46003  cncfiooicclem1  46005  cncfiooiccre  46007  cncfioobd  46009  dvsubcncf  46036  dvmulcncf  46037  dvdivcncf  46039  ioodvbdlimc1lem1  46043  cnbdibl  46074  itgsubsticclem  46087  itgsubsticc  46088  itgioocnicc  46089  iblcncfioo  46090  itgiccshift  46092  itgsbtaddcnst  46094  fourierdlem18  46237  fourierdlem32  46251  fourierdlem33  46252  fourierdlem39  46258  fourierdlem48  46266  fourierdlem49  46267  fourierdlem58  46276  fourierdlem59  46277  fourierdlem71  46289  fourierdlem73  46291  fourierdlem81  46299  fourierdlem84  46302  fourierdlem85  46303  fourierdlem88  46306  fourierdlem94  46312  fourierdlem97  46315  fourierdlem101  46319  fourierdlem103  46321  fourierdlem104  46322  fourierdlem111  46329  fourierdlem112  46330  fourierdlem113  46331  fouriercn  46344