Theorem cncff 23501

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∈ wcel 2114  ∀wral 3138  ∃wrex 3139   ⊆ wss 3936   class class class wbr 5066  ⟶wf 6351  ‘cfv 6355  (class class class)co 7156  ℂcc 10535   < clt 10675   − cmin 10870  ℝ⁺crp 12390  abscabs 14593  –cn→ccncf 23484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161  df-map 8408  df-cncf 23486

This theorem is referenced by:  cncfss  23507  climcncf  23508  cncfco  23515  cncfmpt1f  23521  cncfmpt2ss  23523  negfcncf  23527  divcncf  24048  ivth2  24056  ivthicc  24059  evthicc2  24061  cniccbdd  24062  volivth  24208  cncombf  24259  cnmbf  24260  cniccibl  24441  cnmptlimc  24488  cpnord  24532  cpnres  24534  dvrec  24552  rollelem  24586  rolle  24587  cmvth  24588  mvth  24589  dvlip  24590  c1liplem1  24593  c1lip1  24594  c1lip2  24595  dveq0  24597  dvgt0lem1  24599  dvgt0lem2  24600  dvgt0  24601  dvlt0  24602  dvge0  24603  dvle  24604  dvivthlem1  24605  dvivth  24607  dvne0  24608  dvne0f1  24609  dvcnvrelem1  24614  dvcnvrelem2  24615  dvcnvre  24616  dvcvx  24617  dvfsumle  24618  dvfsumge  24619  dvfsumabs  24620  ftc1cn  24640  ftc2  24641  ftc2ditglem  24642  ftc2ditg  24643  itgparts  24644  itgsubstlem  24645  itgsubst  24646  ulmcn  24987  psercn  25014  pserdvlem2  25016  pserdv  25017  sincn  25032  coscn  25033  logtayl  25243  dvcncxp1  25324  leibpi  25520  lgamgulmlem2  25607  ftc2re  31869  fdvposlt  31870  fdvneggt  31871  fdvposle  31872  fdvnegge  31873  ivthALT  33683  knoppcld  33844  knoppndv  33873  cnicciblnc  34978  ftc1cnnclem  34980  ftc1cnnc  34981  ftc2nc  34991  cnioobibld  39869  evthiccabs  41820  cncfmptss  41917  mulc1cncfg  41919  expcnfg  41921  mulcncff  42200  cncfshift  42206  subcncff  42212  cncfcompt  42215  addcncff  42216  cncficcgt0  42220  divcncff  42223  cncfiooicclem1  42225  cncfiooiccre  42227  cncfioobd  42229  cncfcompt2  42231  dvsubcncf  42258  dvmulcncf  42259  dvdivcncf  42261  ioodvbdlimc1lem1  42265  cnbdibl  42296  itgsubsticclem  42309  itgsubsticc  42310  itgioocnicc  42311  iblcncfioo  42312  itgiccshift  42314  itgsbtaddcnst  42316  fourierdlem18  42459  fourierdlem32  42473  fourierdlem33  42474  fourierdlem39  42480  fourierdlem48  42488  fourierdlem49  42489  fourierdlem58  42498  fourierdlem59  42499  fourierdlem71  42511  fourierdlem73  42513  fourierdlem81  42521  fourierdlem84  42524  fourierdlem85  42525  fourierdlem88  42528  fourierdlem94  42534  fourierdlem97  42537  fourierdlem101  42541  fourierdlem103  42543  fourierdlem104  42544  fourierdlem111  42551  fourierdlem112  42552  fourierdlem113  42553  fouriercn  42566