Theorem cncff 25244

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 25242	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
2		cncfrss2 25243	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
3		elcncf 25240	. . . 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 2147  ∀wral 3080  ∃wrex 3090   ⊆ wss 3900   class class class wbr 5106  ⟶wf 6554  ‘cfv 6558  (class class class)co 7443  ℂcc 11225   < clt 11370   − cmin 11568  ℝ⁺crp 13147  abscabs 15430  –cn→ccncf 25227

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-cnex 11283

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-fv 6566  df-ov 7446  df-oprab 7447  df-mpo 7448  df-map 8877  df-cncf 25229

This theorem is used by:  cncfss  25250  climcncf  25251  cncfco  25258  cncfcompt2  25259  cncfmpt1f  25265  cncfmpt2ss  25267  negfcncf  25274  divcncf  25798  ivth2  25806  ivthicc  25809  evthicc2  25811  cniccbdd  25812  volivth  25958  cncombf  26009  cnmbf  26010  cniccibl  26191  cnicciblnc  26193  cnmptlimc  26240  cpnord  26285  cpnres  26287  dvrec  26305  rollelem  26339  rolle  26340  cmvth  26341  mvth  26342  dvlip  26343  c1liplem1  26346  c1lip1  26347  c1lip2  26348  dveq0  26350  dvgt0lem1  26352  dvgt0lem2  26353  dvgt0  26354  dvlt0  26355  dvge0  26356  dvle  26357  dvivthlem1  26358  dvivth  26360  dvne0  26361  dvne0f1  26362  dvcnvrelem1  26367  dvcnvrelem2  26368  dvcnvre  26369  dvcvx  26370  dvfsumle  26371  dvfsumge  26372  dvfsumabs  26373  ftc1cn  26393  ftc2  26394  ftc2ditglem  26395  ftc2ditg  26396  itgparts  26397  itgsubstlem  26398  itgsubst  26399  ulmcn  26756  psercn  26783  pserdvlem2  26785  pserdv  26786  sincn  26801  coscn  26802  logtayl  27018  dvcncxp1  27101  leibpi  27300  lgamgulmlem2  27387  ftc2re  35297  fdvposlt  35298  fdvneggt  35299  fdvposle  35300  fdvnegge  35301  ivthALT  37301  knoppcld  37549  knoppndv  37578  ftc1cnnclem  38801  ftc1cnnc  38802  ftc2nc  38812  3factsumint  43267  intlewftc  43303  dvle2  43314  cnioobibld  44408  evthiccabs  46713  cncfmptss  46804  mulc1cncfg  46806  expcnfg  46808  mulcncff  47085  cncfshift  47089  subcncff  47095  cncfcompt  47098  addcncff  47099  cncficcgt0  47103  divcncff  47106  cncfiooicclem1  47108  cncfiooiccre  47110  cncfioobd  47112  dvsubcncf  47139  dvmulcncf  47140  dvdivcncf  47142  ioodvbdlimc1lem1  47146  cnbdibl  47177  itgsubsticclem  47190  itgsubsticc  47191  itgioocnicc  47192  iblcncfioo  47193  itgiccshift  47195  itgsbtaddcnst  47197  fourierdlem18  47340  fourierdlem32  47354  fourierdlem33  47355  fourierdlem39  47361  fourierdlem48  47369  fourierdlem49  47370  fourierdlem58  47379  fourierdlem59  47380  fourierdlem71  47392  fourierdlem73  47394  fourierdlem81  47402  fourierdlem84  47405  fourierdlem85  47406  fourierdlem88  47409  fourierdlem94  47415  fourierdlem97  47418  fourierdlem101  47422  fourierdlem103  47424  fourierdlem104  47425  fourierdlem111  47432  fourierdlem112  47433  fourierdlem113  47434  fouriercn  47447