Theorem cncff 25214

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087   ⊆ wss 3899   class class class wbr 5103  ⟶wf 6534  ‘cfv 6538  (class class class)co 7420  ℂcc 11198   < clt 11343   − cmin 11541  ℝ⁺crp 13120  abscabs 15401  –cn→ccncf 25197

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-cnex 11256

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-map 8849  df-cncf 25199

This theorem is used by:  cncfss  25220  climcncf  25221  cncfco  25228  cncfcompt2  25229  cncfmpt1f  25235  cncfmpt2ss  25237  negfcncf  25244  divcncf  25768  ivth2  25776  ivthicc  25779  evthicc2  25781  cniccbdd  25782  volivth  25928  cncombf  25979  cnmbf  25980  cniccibl  26161  cnicciblnc  26163  cnmptlimc  26210  cpnord  26255  cpnres  26257  dvrec  26275  rollelem  26309  rolle  26310  cmvth  26311  mvth  26312  dvlip  26313  c1liplem1  26316  c1lip1  26317  c1lip2  26318  dveq0  26320  dvgt0lem1  26322  dvgt0lem2  26323  dvgt0  26324  dvlt0  26325  dvge0  26326  dvle  26327  dvivthlem1  26328  dvivth  26330  dvne0  26331  dvne0f1  26332  dvcnvrelem1  26337  dvcnvrelem2  26338  dvcnvre  26339  dvcvx  26340  dvfsumle  26341  dvfsumge  26342  dvfsumabs  26343  ftc1cn  26363  ftc2  26364  ftc2ditglem  26365  ftc2ditg  26366  itgparts  26367  itgsubstlem  26368  itgsubst  26369  ulmcn  26726  psercn  26753  pserdvlem2  26755  pserdv  26756  sincn  26771  coscn  26772  logtayl  26988  dvcncxp1  27071  leibpi  27270  lgamgulmlem2  27357  ftc2re  35227  fdvposlt  35228  fdvneggt  35229  fdvposle  35230  fdvnegge  35231  ivthALT  37123  knoppcld  37371  knoppndv  37400  ftc1cnnclem  38609  ftc1cnnc  38610  ftc2nc  38620  3factsumint  43075  intlewftc  43111  dvle2  43122  cnioobibld  44215  evthiccabs  46507  cncfmptss  46598  mulc1cncfg  46600  expcnfg  46602  mulcncff  46879  cncfshift  46883  subcncff  46889  cncfcompt  46892  addcncff  46893  cncficcgt0  46897  divcncff  46900  cncfiooicclem1  46902  cncfiooiccre  46904  cncfioobd  46906  dvsubcncf  46933  dvmulcncf  46934  dvdivcncf  46936  ioodvbdlimc1lem1  46940  cnbdibl  46971  itgsubsticclem  46984  itgsubsticc  46985  itgioocnicc  46986  iblcncfioo  46987  itgiccshift  46989  itgsbtaddcnst  46991  fourierdlem18  47134  fourierdlem32  47148  fourierdlem33  47149  fourierdlem39  47155  fourierdlem48  47163  fourierdlem49  47164  fourierdlem58  47173  fourierdlem59  47174  fourierdlem71  47186  fourierdlem73  47188  fourierdlem81  47196  fourierdlem84  47199  fourierdlem85  47200  fourierdlem88  47203  fourierdlem94  47209  fourierdlem97  47212  fourierdlem101  47216  fourierdlem103  47218  fourierdlem104  47219  fourierdlem111  47226  fourierdlem112  47227  fourierdlem113  47228  fouriercn  47241