Theorem cncff 24835

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 24833	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
2		cncfrss2 24834	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
3		elcncf 24831	. . . 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 2108  ∀wral 3051  ∃wrex 3060   ⊆ wss 3926   class class class wbr 5119  ⟶wf 6526  ‘cfv 6530  (class class class)co 7403  ℂcc 11125   < clt 11267   − cmin 11464  ℝ⁺crp 13006  abscabs 15251  –cn→ccncf 24818

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-fv 6538  df-ov 7406  df-oprab 7407  df-mpo 7408  df-map 8840  df-cncf 24820

This theorem is referenced by:  cncfss  24841  climcncf  24842  cncfco  24849  cncfcompt2  24850  cncfmpt1f  24856  cncfmpt2ss  24858  negfcncf  24866  divcncf  25398  ivth2  25406  ivthicc  25409  evthicc2  25411  cniccbdd  25412  volivth  25558  cncombf  25609  cnmbf  25610  cniccibl  25792  cnicciblnc  25794  cnmptlimc  25841  cpnord  25887  cpnres  25889  dvrec  25909  rollelem  25943  rolle  25944  cmvth  25945  cmvthOLD  25946  mvth  25947  dvlip  25948  c1liplem1  25951  c1lip1  25952  c1lip2  25953  dveq0  25955  dvgt0lem1  25957  dvgt0lem2  25958  dvgt0  25959  dvlt0  25960  dvge0  25961  dvle  25962  dvivthlem1  25963  dvivth  25965  dvne0  25966  dvne0f1  25967  dvcnvrelem1  25972  dvcnvrelem2  25973  dvcnvre  25974  dvcvx  25975  dvfsumle  25976  dvfsumleOLD  25977  dvfsumge  25978  dvfsumabs  25979  ftc1cn  26000  ftc2  26001  ftc2ditglem  26002  ftc2ditg  26003  itgparts  26004  itgsubstlem  26005  itgsubst  26006  ulmcn  26358  psercn  26386  pserdvlem2  26388  pserdv  26389  sincn  26404  coscn  26405  logtayl  26619  dvcncxp1  26702  leibpi  26902  lgamgulmlem2  26990  ftc2re  34576  fdvposlt  34577  fdvneggt  34578  fdvposle  34579  fdvnegge  34580  ivthALT  36299  knoppcld  36469  knoppndv  36498  ftc1cnnclem  37661  ftc1cnnc  37662  ftc2nc  37672  3factsumint  41984  intlewftc  42020  dvle2  42031  cnioobibld  43185  evthiccabs  45473  cncfmptss  45564  mulc1cncfg  45566  expcnfg  45568  mulcncff  45847  cncfshift  45851  subcncff  45857  cncfcompt  45860  addcncff  45861  cncficcgt0  45865  divcncff  45868  cncfiooicclem1  45870  cncfiooiccre  45872  cncfioobd  45874  dvsubcncf  45901  dvmulcncf  45902  dvdivcncf  45904  ioodvbdlimc1lem1  45908  cnbdibl  45939  itgsubsticclem  45952  itgsubsticc  45953  itgioocnicc  45954  iblcncfioo  45955  itgiccshift  45957  itgsbtaddcnst  45959  fourierdlem18  46102  fourierdlem32  46116  fourierdlem33  46117  fourierdlem39  46123  fourierdlem48  46131  fourierdlem49  46132  fourierdlem58  46141  fourierdlem59  46142  fourierdlem71  46154  fourierdlem73  46156  fourierdlem81  46164  fourierdlem84  46167  fourierdlem85  46168  fourierdlem88  46171  fourierdlem94  46177  fourierdlem97  46180  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fourierdlem112  46195  fourierdlem113  46196  fouriercn  46209