Theorem cncff 23189

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∈ wcel 2081  ∀wral 3105  ∃wrex 3106   ⊆ wss 3863   class class class wbr 4966  ⟶wf 6226  ‘cfv 6230  (class class class)co 7021  ℂcc 10386   < clt 10526   − cmin 10722  ℝ⁺crp 12244  abscabs 14432  –cn→ccncf 23172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226  ax-un 7324  ax-cnex 10444

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3710  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-pw 4459  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-br 4967  df-opab 5029  df-id 5353  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-fv 6238  df-ov 7024  df-oprab 7025  df-mpo 7026  df-map 8263  df-cncf 23174

This theorem is referenced by:  cncfss  23195  climcncf  23196  cncfco  23203  cncfmpt1f  23209  cncfmpt2ss  23211  negfcncf  23215  divcncf  23736  ivth2  23744  ivthicc  23747  evthicc2  23749  cniccbdd  23750  volivth  23896  cncombf  23947  cnmbf  23948  cniccibl  24129  cnmptlimc  24176  cpnord  24220  cpnres  24222  dvrec  24240  rollelem  24274  rolle  24275  cmvth  24276  mvth  24277  dvlip  24278  c1liplem1  24281  c1lip1  24282  c1lip2  24283  dveq0  24285  dvgt0lem1  24287  dvgt0lem2  24288  dvgt0  24289  dvlt0  24290  dvge0  24291  dvle  24292  dvivthlem1  24293  dvivth  24295  dvne0  24296  dvne0f1  24297  dvcnvrelem1  24302  dvcnvrelem2  24303  dvcnvre  24304  dvcvx  24305  dvfsumle  24306  dvfsumge  24307  dvfsumabs  24308  ftc1cn  24328  ftc2  24329  ftc2ditglem  24330  ftc2ditg  24331  itgparts  24332  itgsubstlem  24333  itgsubst  24334  ulmcn  24675  psercn  24702  pserdvlem2  24704  pserdv  24705  sincn  24720  coscn  24721  logtayl  24929  dvcncxp1  25010  leibpi  25207  lgamgulmlem2  25294  ftc2re  31491  fdvposlt  31492  fdvneggt  31493  fdvposle  31494  fdvnegge  31495  ivthALT  33298  knoppcld  33459  knoppndv  33488  cnicciblnc  34519  ftc1cnnclem  34521  ftc1cnnc  34522  ftc2nc  34532  cnioobibld  39330  evthiccabs  41338  cncfmptss  41435  mulc1cncfg  41437  expcnfg  41439  mulcncff  41718  cncfshift  41724  subcncff  41730  cncfcompt  41733  addcncff  41734  cncficcgt0  41738  divcncff  41741  cncfiooicclem1  41743  cncfiooiccre  41745  cncfioobd  41747  cncfcompt2  41749  dvsubcncf  41776  dvmulcncf  41777  dvdivcncf  41779  ioodvbdlimc1lem1  41783  cnbdibl  41814  itgsubsticclem  41827  itgsubsticc  41828  itgioocnicc  41829  iblcncfioo  41830  itgiccshift  41832  itgsbtaddcnst  41834  fourierdlem18  41978  fourierdlem32  41992  fourierdlem33  41993  fourierdlem39  41999  fourierdlem48  42007  fourierdlem49  42008  fourierdlem58  42017  fourierdlem59  42018  fourierdlem71  42030  fourierdlem73  42032  fourierdlem81  42040  fourierdlem84  42043  fourierdlem85  42044  fourierdlem88  42047  fourierdlem94  42053  fourierdlem97  42056  fourierdlem101  42060  fourierdlem103  42062  fourierdlem104  42063  fourierdlem111  42070  fourierdlem112  42071  fourierdlem113  42072  fouriercn  42085