Theorem cncff 24885

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 24883	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
2		cncfrss2 24884	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
3		elcncf 24881	. . . 4 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))))
4	1, 2, 3	syl2anc 590	. . 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 2119  ∀wral 3054  ∃wrex 3064   ⊆ wss 3890   class class class wbr 5079  ⟶wf 6488  ‘cfv 6492  (class class class)co 7363  ℂcc 11034   < clt 11177   − cmin 11375  ℝ⁺crp 12940  abscabs 15194  –cn→ccncf 24868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-cnex 11092

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-map 8772  df-cncf 24870

This theorem is referenced by:  cncfss  24891  climcncf  24892  cncfco  24899  cncfcompt2  24900  cncfmpt1f  24906  cncfmpt2ss  24908  negfcncf  24915  divcncf  25439  ivth2  25447  ivthicc  25450  evthicc2  25452  cniccbdd  25453  volivth  25599  cncombf  25650  cnmbf  25651  cniccibl  25833  cnicciblnc  25835  cnmptlimc  25882  cpnord  25927  cpnres  25929  dvrec  25947  rollelem  25981  rolle  25982  cmvth  25983  mvth  25984  dvlip  25985  c1liplem1  25988  c1lip1  25989  c1lip2  25990  dveq0  25992  dvgt0lem1  25994  dvgt0lem2  25995  dvgt0  25996  dvlt0  25997  dvge0  25998  dvle  25999  dvivthlem1  26000  dvivth  26002  dvne0  26003  dvne0f1  26004  dvcnvrelem1  26009  dvcnvrelem2  26010  dvcnvre  26011  dvcvx  26012  dvfsumle  26013  dvfsumge  26014  dvfsumabs  26015  ftc1cn  26035  ftc2  26036  ftc2ditglem  26037  ftc2ditg  26038  itgparts  26039  itgsubstlem  26040  itgsubst  26041  ulmcn  26389  psercn  26416  pserdvlem2  26418  pserdv  26419  sincn  26434  coscn  26435  logtayl  26649  dvcncxp1  26732  leibpi  26931  lgamgulmlem2  27018  ftc2re  34789  fdvposlt  34790  fdvneggt  34791  fdvposle  34792  fdvnegge  34793  ivthALT  36564  knoppcld  36812  knoppndv  36841  ftc1cnnclem  38059  ftc1cnnc  38060  ftc2nc  38070  3factsumint  42511  intlewftc  42547  dvle2  42558  cnioobibld  43660  evthiccabs  45942  cncfmptss  46033  mulc1cncfg  46035  expcnfg  46037  mulcncff  46314  cncfshift  46318  subcncff  46324  cncfcompt  46327  addcncff  46328  cncficcgt0  46332  divcncff  46335  cncfiooicclem1  46337  cncfiooiccre  46339  cncfioobd  46341  dvsubcncf  46368  dvmulcncf  46369  dvdivcncf  46371  ioodvbdlimc1lem1  46375  cnbdibl  46406  itgsubsticclem  46419  itgsubsticc  46420  itgioocnicc  46421  iblcncfioo  46422  itgiccshift  46424  itgsbtaddcnst  46426  fourierdlem18  46569  fourierdlem32  46583  fourierdlem33  46584  fourierdlem39  46590  fourierdlem48  46598  fourierdlem49  46599  fourierdlem58  46608  fourierdlem59  46609  fourierdlem71  46621  fourierdlem73  46623  fourierdlem81  46631  fourierdlem84  46634  fourierdlem85  46635  fourierdlem88  46638  fourierdlem94  46644  fourierdlem97  46647  fourierdlem101  46651  fourierdlem103  46653  fourierdlem104  46654  fourierdlem111  46661  fourierdlem112  46662  fourierdlem113  46663  fouriercn  46676