Theorem cncff 25176

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 25174	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ)
2		cncfrss2 25175	. . . 4 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ)
3		elcncf 25172	. . . 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 3076  ∃wrex 3086   ⊆ wss 3898   class class class wbr 5102  ⟶wf 6523  ‘cfv 6527  (class class class)co 7408  ℂcc 11170   < clt 11315   − cmin 11513  ℝ⁺crp 13090  abscabs 15369  –cn→ccncf 25159

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 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-cnex 11228

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-fv 6535  df-ov 7411  df-oprab 7412  df-mpo 7413  df-map 8827  df-cncf 25161

This theorem is used by:  cncfss  25182  climcncf  25183  cncfco  25190  cncfcompt2  25191  cncfmpt1f  25197  cncfmpt2ss  25199  negfcncf  25206  divcncf  25730  ivth2  25738  ivthicc  25741  evthicc2  25743  cniccbdd  25744  volivth  25890  cncombf  25941  cnmbf  25942  cniccibl  26123  cnicciblnc  26125  cnmptlimc  26172  cpnord  26217  cpnres  26219  dvrec  26237  rollelem  26271  rolle  26272  cmvth  26273  mvth  26274  dvlip  26275  c1liplem1  26278  c1lip1  26279  c1lip2  26280  dveq0  26282  dvgt0lem1  26284  dvgt0lem2  26285  dvgt0  26286  dvlt0  26287  dvge0  26288  dvle  26289  dvivthlem1  26290  dvivth  26292  dvne0  26293  dvne0f1  26294  dvcnvrelem1  26299  dvcnvrelem2  26300  dvcnvre  26301  dvcvx  26302  dvfsumle  26303  dvfsumge  26304  dvfsumabs  26305  ftc1cn  26325  ftc2  26326  ftc2ditglem  26327  ftc2ditg  26328  itgparts  26329  itgsubstlem  26330  itgsubst  26331  ulmcn  26690  psercn  26717  pserdvlem2  26719  pserdv  26720  sincn  26735  coscn  26736  logtayl  26952  dvcncxp1  27035  leibpi  27234  lgamgulmlem2  27321  ftc2re  35162  fdvposlt  35163  fdvneggt  35164  fdvposle  35165  fdvnegge  35166  ivthALT  37045  knoppcld  37293  knoppndv  37322  ftc1cnnclem  38529  ftc1cnnc  38530  ftc2nc  38540  3factsumint  42995  intlewftc  43031  dvle2  43042  cnioobibld  44159  evthiccabs  46430  cncfmptss  46521  mulc1cncfg  46523  expcnfg  46525  mulcncff  46802  cncfshift  46806  subcncff  46812  cncfcompt  46815  addcncff  46816  cncficcgt0  46820  divcncff  46823  cncfiooicclem1  46825  cncfiooiccre  46827  cncfioobd  46829  dvsubcncf  46856  dvmulcncf  46857  dvdivcncf  46859  ioodvbdlimc1lem1  46863  cnbdibl  46894  itgsubsticclem  46907  itgsubsticc  46908  itgioocnicc  46909  iblcncfioo  46910  itgiccshift  46912  itgsbtaddcnst  46914  fourierdlem18  47057  fourierdlem32  47071  fourierdlem33  47072  fourierdlem39  47078  fourierdlem48  47086  fourierdlem49  47087  fourierdlem58  47096  fourierdlem59  47097  fourierdlem71  47109  fourierdlem73  47111  fourierdlem81  47119  fourierdlem84  47122  fourierdlem85  47123  fourierdlem88  47126  fourierdlem94  47132  fourierdlem97  47135  fourierdlem101  47139  fourierdlem103  47141  fourierdlem104  47142  fourierdlem111  47149  fourierdlem112  47150  fourierdlem113  47151  fouriercn  47164