Theorem cncff 24928

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∈ wcel 2136  ∀wral 3070  ∃wrex 3080   ⊆ wss 3899   class class class wbr 5094  ⟶wf 6506  ‘cfv 6510  (class class class)co 7385  ℂcc 11061   < clt 11206   − cmin 11404  ℝ⁺crp 12983  abscabs 15237  –cn→ccncf 24911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728  ax-sep 5240  ax-nul 5250  ax-pow 5316  ax-pr 5384  ax-un 7707  ax-cnex 11119

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-mo 2560  df-eu 2590  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-ne 2952  df-ral 3071  df-rex 3081  df-rab 3409  df-v 3450  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-pw 4551  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-opab 5157  df-id 5535  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-iota 6466  df-fun 6512  df-fn 6513  df-f 6514  df-fv 6518  df-ov 7388  df-oprab 7389  df-mpo 7390  df-map 8798  df-cncf 24913

This theorem is referenced by:  cncfss  24934  climcncf  24935  cncfco  24942  cncfcompt2  24943  cncfmpt1f  24949  cncfmpt2ss  24951  negfcncf  24958  divcncf  25482  ivth2  25490  ivthicc  25493  evthicc2  25495  cniccbdd  25496  volivth  25642  cncombf  25693  cnmbf  25694  cniccibl  25876  cnicciblnc  25878  cnmptlimc  25925  cpnord  25970  cpnres  25972  dvrec  25990  rollelem  26024  rolle  26025  cmvth  26026  mvth  26027  dvlip  26028  c1liplem1  26031  c1lip1  26032  c1lip2  26033  dveq0  26035  dvgt0lem1  26037  dvgt0lem2  26038  dvgt0  26039  dvlt0  26040  dvge0  26041  dvle  26042  dvivthlem1  26043  dvivth  26045  dvne0  26046  dvne0f1  26047  dvcnvrelem1  26052  dvcnvrelem2  26053  dvcnvre  26054  dvcvx  26055  dvfsumle  26056  dvfsumge  26057  dvfsumabs  26058  ftc1cn  26078  ftc2  26079  ftc2ditglem  26080  ftc2ditg  26081  itgparts  26082  itgsubstlem  26083  itgsubst  26084  ulmcn  26432  psercn  26459  pserdvlem2  26461  pserdv  26462  sincn  26477  coscn  26478  logtayl  26695  dvcncxp1  26778  leibpi  26977  lgamgulmlem2  27064  ftc2re  34849  fdvposlt  34850  fdvneggt  34851  fdvposle  34852  fdvnegge  34853  ivthALT  36643  knoppcld  36891  knoppndv  36920  ftc1cnnclem  38138  ftc1cnnc  38139  ftc2nc  38149  3factsumint  42590  intlewftc  42626  dvle2  42637  cnioobibld  43739  evthiccabs  46020  cncfmptss  46111  mulc1cncfg  46113  expcnfg  46115  mulcncff  46392  cncfshift  46396  subcncff  46402  cncfcompt  46405  addcncff  46406  cncficcgt0  46410  divcncff  46413  cncfiooicclem1  46415  cncfiooiccre  46417  cncfioobd  46419  dvsubcncf  46446  dvmulcncf  46447  dvdivcncf  46449  ioodvbdlimc1lem1  46453  cnbdibl  46484  itgsubsticclem  46497  itgsubsticc  46498  itgioocnicc  46499  iblcncfioo  46500  itgiccshift  46502  itgsbtaddcnst  46504  fourierdlem18  46647  fourierdlem32  46661  fourierdlem33  46662  fourierdlem39  46668  fourierdlem48  46676  fourierdlem49  46677  fourierdlem58  46686  fourierdlem59  46687  fourierdlem71  46699  fourierdlem73  46701  fourierdlem81  46709  fourierdlem84  46712  fourierdlem85  46713  fourierdlem88  46716  fourierdlem94  46722  fourierdlem97  46725  fourierdlem101  46729  fourierdlem103  46731  fourierdlem104  46732  fourierdlem111  46739  fourierdlem112  46740  fourierdlem113  46741  fouriercn  46754