Theorem cncff 22504

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897   ⊆ wss 3540   class class class wbr 4583  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  ℂcc 9813   < clt 9953   − cmin 10145  ℝ⁺crp 11708  abscabs 13822  –cn→ccncf 22487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-map 7746  df-cncf 22489

This theorem is referenced by:  cncfss  22510  climcncf  22511  cncfco  22518  cncfmpt1f  22524  cncfmpt2ss  22526  negfcncf  22530  ivth2  23031  ivthicc  23034  evthicc2  23036  cniccbdd  23037  volivth  23181  cncombf  23231  cnmbf  23232  cniccibl  23413  cnmptlimc  23460  cpnord  23504  cpnres  23506  dvrec  23524  rollelem  23556  rolle  23557  cmvth  23558  mvth  23559  dvlip  23560  c1liplem1  23563  c1lip1  23564  c1lip2  23565  dveq0  23567  dvgt0lem1  23569  dvgt0lem2  23570  dvgt0  23571  dvlt0  23572  dvge0  23573  dvle  23574  dvivthlem1  23575  dvivth  23577  dvne0  23578  dvne0f1  23579  dvcnvrelem1  23584  dvcnvrelem2  23585  dvcnvre  23586  dvcvx  23587  dvfsumle  23588  dvfsumge  23589  dvfsumabs  23590  ftc1cn  23610  ftc2  23611  ftc2ditglem  23612  ftc2ditg  23613  itgparts  23614  itgsubstlem  23615  itgsubst  23616  ulmcn  23957  psercn  23984  pserdvlem2  23986  pserdv  23987  sincn  24002  coscn  24003  logtayl  24206  dvcncxp1  24284  leibpi  24469  lgamgulmlem2  24556  ivthALT  31500  knoppcld  31665  knoppndv  31695  cnicciblnc  32651  ftc1cnnclem  32653  ftc1cnnc  32654  ftc2nc  32664  cnioobibld  36818  evthiccabs  38565  cncfmptss  38654  mulc1cncfg  38656  expcnfg  38658  mulcncff  38753  cncfshift  38759  subcncff  38765  cncfcompt  38768  divcncf  38769  addcncff  38770  cncficcgt0  38774  divcncff  38777  cncfiooicclem1  38779  cncfiooiccre  38781  cncfioobd  38783  cncfcompt2  38785  dvsubcncf  38814  dvmulcncf  38815  dvdivcncf  38817  ioodvbdlimc1lem1  38821  cnbdibl  38854  itgsubsticclem  38867  itgsubsticc  38868  itgioocnicc  38869  iblcncfioo  38870  itgiccshift  38872  itgsbtaddcnst  38874  fourierdlem18  39018  fourierdlem32  39032  fourierdlem33  39033  fourierdlem39  39039  fourierdlem48  39047  fourierdlem49  39048  fourierdlem58  39057  fourierdlem59  39058  fourierdlem71  39070  fourierdlem73  39072  fourierdlem81  39080  fourierdlem84  39083  fourierdlem85  39084  fourierdlem88  39087  fourierdlem94  39093  fourierdlem97  39096  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem112  39111  fourierdlem113  39112  fouriercn  39125