Theorem cncff 24869

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 24867	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
2		cncfrss2 24868	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
3		elcncf 24865	. . . 4 ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))))
4	1, 2, 3	syl2anc 585	. . 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 2114  ∀wral 3052  ∃wrex 3062   ⊆ wss 3890   class class class wbr 5086  ⟶wf 6486  ‘cfv 6490  (class class class)co 7358  ℂcc 11025   < clt 11168   − cmin 11366  ℝ⁺crp 12931  abscabs 15185  –cn→ccncf 24852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-cnex 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498  df-ov 7361  df-oprab 7362  df-mpo 7363  df-map 8766  df-cncf 24854

This theorem is referenced by:  cncfss  24875  climcncf  24876  cncfco  24883  cncfcompt2  24884  cncfmpt1f  24890  cncfmpt2ss  24892  negfcncf  24899  divcncf  25423  ivth2  25431  ivthicc  25434  evthicc2  25436  cniccbdd  25437  volivth  25583  cncombf  25634  cnmbf  25635  cniccibl  25817  cnicciblnc  25819  cnmptlimc  25866  cpnord  25911  cpnres  25913  dvrec  25931  rollelem  25965  rolle  25966  cmvth  25967  cmvthOLD  25968  mvth  25969  dvlip  25970  c1liplem1  25973  c1lip1  25974  c1lip2  25975  dveq0  25977  dvgt0lem1  25979  dvgt0lem2  25980  dvgt0  25981  dvlt0  25982  dvge0  25983  dvle  25984  dvivthlem1  25985  dvivth  25987  dvne0  25988  dvne0f1  25989  dvcnvrelem1  25994  dvcnvrelem2  25995  dvcnvre  25996  dvcvx  25997  dvfsumle  25998  dvfsumleOLD  25999  dvfsumge  26000  dvfsumabs  26001  ftc1cn  26022  ftc2  26023  ftc2ditglem  26024  ftc2ditg  26025  itgparts  26026  itgsubstlem  26027  itgsubst  26028  ulmcn  26379  psercn  26407  pserdvlem2  26409  pserdv  26410  sincn  26425  coscn  26426  logtayl  26640  dvcncxp1  26723  leibpi  26923  lgamgulmlem2  27011  ftc2re  34763  fdvposlt  34764  fdvneggt  34765  fdvposle  34766  fdvnegge  34767  ivthALT  36538  knoppcld  36778  knoppndv  36807  ftc1cnnclem  38023  ftc1cnnc  38024  ftc2nc  38034  3factsumint  42475  intlewftc  42511  dvle2  42522  cnioobibld  43657  evthiccabs  45941  cncfmptss  46032  mulc1cncfg  46034  expcnfg  46036  mulcncff  46313  cncfshift  46317  subcncff  46323  cncfcompt  46326  addcncff  46327  cncficcgt0  46331  divcncff  46334  cncfiooicclem1  46336  cncfiooiccre  46338  cncfioobd  46340  dvsubcncf  46367  dvmulcncf  46368  dvdivcncf  46370  ioodvbdlimc1lem1  46374  cnbdibl  46405  itgsubsticclem  46418  itgsubsticc  46419  itgioocnicc  46420  iblcncfioo  46421  itgiccshift  46423  itgsbtaddcnst  46425  fourierdlem18  46568  fourierdlem32  46582  fourierdlem33  46583  fourierdlem39  46589  fourierdlem48  46597  fourierdlem49  46598  fourierdlem58  46607  fourierdlem59  46608  fourierdlem71  46620  fourierdlem73  46622  fourierdlem81  46630  fourierdlem84  46633  fourierdlem85  46634  fourierdlem88  46637  fourierdlem94  46643  fourierdlem97  46646  fourierdlem101  46650  fourierdlem103  46652  fourierdlem104  46653  fourierdlem111  46660  fourierdlem112  46661  fourierdlem113  46662  fouriercn  46675