Theorem cncff 24793

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 24791	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
2		cncfrss2 24792	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
3		elcncf 24789	. . . 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 2109  ∀wral 3045  ∃wrex 3054   ⊆ wss 3917   class class class wbr 5110  ⟶wf 6510  ‘cfv 6514  (class class class)co 7390  ℂcc 11073   < clt 11215   − cmin 11412  ℝ⁺crp 12958  abscabs 15207  –cn→ccncf 24776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  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 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-map 8804  df-cncf 24778

This theorem is referenced by:  cncfss  24799  climcncf  24800  cncfco  24807  cncfcompt2  24808  cncfmpt1f  24814  cncfmpt2ss  24816  negfcncf  24824  divcncf  25355  ivth2  25363  ivthicc  25366  evthicc2  25368  cniccbdd  25369  volivth  25515  cncombf  25566  cnmbf  25567  cniccibl  25749  cnicciblnc  25751  cnmptlimc  25798  cpnord  25844  cpnres  25846  dvrec  25866  rollelem  25900  rolle  25901  cmvth  25902  cmvthOLD  25903  mvth  25904  dvlip  25905  c1liplem1  25908  c1lip1  25909  c1lip2  25910  dveq0  25912  dvgt0lem1  25914  dvgt0lem2  25915  dvgt0  25916  dvlt0  25917  dvge0  25918  dvle  25919  dvivthlem1  25920  dvivth  25922  dvne0  25923  dvne0f1  25924  dvcnvrelem1  25929  dvcnvrelem2  25930  dvcnvre  25931  dvcvx  25932  dvfsumle  25933  dvfsumleOLD  25934  dvfsumge  25935  dvfsumabs  25936  ftc1cn  25957  ftc2  25958  ftc2ditglem  25959  ftc2ditg  25960  itgparts  25961  itgsubstlem  25962  itgsubst  25963  ulmcn  26315  psercn  26343  pserdvlem2  26345  pserdv  26346  sincn  26361  coscn  26362  logtayl  26576  dvcncxp1  26659  leibpi  26859  lgamgulmlem2  26947  ftc2re  34596  fdvposlt  34597  fdvneggt  34598  fdvposle  34599  fdvnegge  34600  ivthALT  36330  knoppcld  36500  knoppndv  36529  ftc1cnnclem  37692  ftc1cnnc  37693  ftc2nc  37703  3factsumint  42020  intlewftc  42056  dvle2  42067  cnioobibld  43210  evthiccabs  45501  cncfmptss  45592  mulc1cncfg  45594  expcnfg  45596  mulcncff  45875  cncfshift  45879  subcncff  45885  cncfcompt  45888  addcncff  45889  cncficcgt0  45893  divcncff  45896  cncfiooicclem1  45898  cncfiooiccre  45900  cncfioobd  45902  dvsubcncf  45929  dvmulcncf  45930  dvdivcncf  45932  ioodvbdlimc1lem1  45936  cnbdibl  45967  itgsubsticclem  45980  itgsubsticc  45981  itgioocnicc  45982  iblcncfioo  45983  itgiccshift  45985  itgsbtaddcnst  45987  fourierdlem18  46130  fourierdlem32  46144  fourierdlem33  46145  fourierdlem39  46151  fourierdlem48  46159  fourierdlem49  46160  fourierdlem58  46169  fourierdlem59  46170  fourierdlem71  46182  fourierdlem73  46184  fourierdlem81  46192  fourierdlem84  46195  fourierdlem85  46196  fourierdlem88  46199  fourierdlem94  46205  fourierdlem97  46208  fourierdlem101  46212  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fourierdlem112  46223  fourierdlem113  46224  fouriercn  46237