Theorem cncff 25125

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  ∀wral 3078  ∃wrex 3088   ⊆ wss 3902   class class class wbr 5107  ⟶wf 6533  ‘cfv 6537  (class class class)co 7416  ℂcc 11125   < clt 11270   − cmin 11468  ℝ⁺crp 13044  abscabs 15323  –cn→ccncf 25108

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-cnex 11183

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7419  df-oprab 7420  df-mpo 7421  df-map 8831  df-cncf 25110

This theorem is used by:  cncfss  25131  climcncf  25132  cncfco  25139  cncfcompt2  25140  cncfmpt1f  25146  cncfmpt2ss  25148  negfcncf  25155  divcncf  25679  ivth2  25687  ivthicc  25690  evthicc2  25692  cniccbdd  25693  volivth  25839  cncombf  25890  cnmbf  25891  cniccibl  26073  cnicciblnc  26075  cnmptlimc  26122  cpnord  26167  cpnres  26169  dvrec  26187  rollelem  26221  rolle  26222  cmvth  26223  mvth  26224  dvlip  26225  c1liplem1  26228  c1lip1  26229  c1lip2  26230  dveq0  26232  dvgt0lem1  26234  dvgt0lem2  26235  dvgt0  26236  dvlt0  26237  dvge0  26238  dvle  26239  dvivthlem1  26240  dvivth  26242  dvne0  26243  dvne0f1  26244  dvcnvrelem1  26249  dvcnvrelem2  26250  dvcnvre  26251  dvcvx  26252  dvfsumle  26253  dvfsumge  26254  dvfsumabs  26255  ftc1cn  26275  ftc2  26276  ftc2ditglem  26277  ftc2ditg  26278  itgparts  26279  itgsubstlem  26280  itgsubst  26281  ulmcn  26635  psercn  26662  pserdvlem2  26664  pserdv  26665  sincn  26680  coscn  26681  logtayl  26898  dvcncxp1  26981  leibpi  27180  lgamgulmlem2  27267  ftc2re  35108  fdvposlt  35109  fdvneggt  35110  fdvposle  35111  fdvnegge  35112  ivthALT  36956  knoppcld  37204  knoppndv  37233  ftc1cnnclem  38442  ftc1cnnc  38443  ftc2nc  38453  3factsumint  42893  intlewftc  42929  dvle2  42940  cnioobibld  44057  evthiccabs  46328  cncfmptss  46419  mulc1cncfg  46421  expcnfg  46423  mulcncff  46700  cncfshift  46704  subcncff  46710  cncfcompt  46713  addcncff  46714  cncficcgt0  46718  divcncff  46721  cncfiooicclem1  46723  cncfiooiccre  46725  cncfioobd  46727  dvsubcncf  46754  dvmulcncf  46755  dvdivcncf  46757  ioodvbdlimc1lem1  46761  cnbdibl  46792  itgsubsticclem  46805  itgsubsticc  46806  itgioocnicc  46807  iblcncfioo  46808  itgiccshift  46810  itgsbtaddcnst  46812  fourierdlem18  46955  fourierdlem32  46969  fourierdlem33  46970  fourierdlem39  46976  fourierdlem48  46984  fourierdlem49  46985  fourierdlem58  46994  fourierdlem59  46995  fourierdlem71  47007  fourierdlem73  47009  fourierdlem81  47017  fourierdlem84  47020  fourierdlem85  47021  fourierdlem88  47024  fourierdlem94  47030  fourierdlem97  47033  fourierdlem101  47037  fourierdlem103  47039  fourierdlem104  47040  fourierdlem111  47047  fourierdlem112  47048  fourierdlem113  47049  fouriercn  47062