Theorem cncff 24806

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 24804	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
2		cncfrss2 24805	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
3		elcncf 24802	. . . 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 2110  ∀wral 3045  ∃wrex 3054   ⊆ wss 3900   class class class wbr 5089  ⟶wf 6473  ‘cfv 6477  (class class class)co 7341  ℂcc 10996   < clt 11138   − cmin 11336  ℝ⁺crp 12882  abscabs 15133  –cn→ccncf 24789

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 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7663  ax-cnex 11054

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 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-sbc 3740  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-opab 5152  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-iota 6433  df-fun 6479  df-fn 6480  df-f 6481  df-fv 6485  df-ov 7344  df-oprab 7345  df-mpo 7346  df-map 8747  df-cncf 24791

This theorem is referenced by:  cncfss  24812  climcncf  24813  cncfco  24820  cncfcompt2  24821  cncfmpt1f  24827  cncfmpt2ss  24829  negfcncf  24837  divcncf  25368  ivth2  25376  ivthicc  25379  evthicc2  25381  cniccbdd  25382  volivth  25528  cncombf  25579  cnmbf  25580  cniccibl  25762  cnicciblnc  25764  cnmptlimc  25811  cpnord  25857  cpnres  25859  dvrec  25879  rollelem  25913  rolle  25914  cmvth  25915  cmvthOLD  25916  mvth  25917  dvlip  25918  c1liplem1  25921  c1lip1  25922  c1lip2  25923  dveq0  25925  dvgt0lem1  25927  dvgt0lem2  25928  dvgt0  25929  dvlt0  25930  dvge0  25931  dvle  25932  dvivthlem1  25933  dvivth  25935  dvne0  25936  dvne0f1  25937  dvcnvrelem1  25942  dvcnvrelem2  25943  dvcnvre  25944  dvcvx  25945  dvfsumle  25946  dvfsumleOLD  25947  dvfsumge  25948  dvfsumabs  25949  ftc1cn  25970  ftc2  25971  ftc2ditglem  25972  ftc2ditg  25973  itgparts  25974  itgsubstlem  25975  itgsubst  25976  ulmcn  26328  psercn  26356  pserdvlem2  26358  pserdv  26359  sincn  26374  coscn  26375  logtayl  26589  dvcncxp1  26672  leibpi  26872  lgamgulmlem2  26960  ftc2re  34601  fdvposlt  34602  fdvneggt  34603  fdvposle  34604  fdvnegge  34605  ivthALT  36348  knoppcld  36518  knoppndv  36547  ftc1cnnclem  37710  ftc1cnnc  37711  ftc2nc  37721  3factsumint  42037  intlewftc  42073  dvle2  42084  cnioobibld  43226  evthiccabs  45515  cncfmptss  45606  mulc1cncfg  45608  expcnfg  45610  mulcncff  45887  cncfshift  45891  subcncff  45897  cncfcompt  45900  addcncff  45901  cncficcgt0  45905  divcncff  45908  cncfiooicclem1  45910  cncfiooiccre  45912  cncfioobd  45914  dvsubcncf  45941  dvmulcncf  45942  dvdivcncf  45944  ioodvbdlimc1lem1  45948  cnbdibl  45979  itgsubsticclem  45992  itgsubsticc  45993  itgioocnicc  45994  iblcncfioo  45995  itgiccshift  45997  itgsbtaddcnst  45999  fourierdlem18  46142  fourierdlem32  46156  fourierdlem33  46157  fourierdlem39  46163  fourierdlem48  46171  fourierdlem49  46172  fourierdlem58  46181  fourierdlem59  46182  fourierdlem71  46194  fourierdlem73  46196  fourierdlem81  46204  fourierdlem84  46207  fourierdlem85  46208  fourierdlem88  46211  fourierdlem94  46217  fourierdlem97  46220  fourierdlem101  46224  fourierdlem103  46226  fourierdlem104  46227  fourierdlem111  46234  fourierdlem112  46235  fourierdlem113  46236  fouriercn  46249