Theorem cncff 22696

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∈ wcel 1990  ∀wral 2912  ∃wrex 2913   ⊆ wss 3574   class class class wbr 4653  ⟶wf 5884  ‘cfv 5888  (class class class)co 6650  ℂcc 9934   < clt 10074   − cmin 10266  ℝ⁺crp 11832  abscabs 13974  –cn→ccncf 22679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-map 7859  df-cncf 22681

This theorem is referenced by:  cncfss  22702  climcncf  22703  cncfco  22710  cncfmpt1f  22716  cncfmpt2ss  22718  negfcncf  22722  divcncf  23216  ivth2  23224  ivthicc  23227  evthicc2  23229  cniccbdd  23230  volivth  23375  cncombf  23425  cnmbf  23426  cniccibl  23607  cnmptlimc  23654  cpnord  23698  cpnres  23700  dvrec  23718  rollelem  23752  rolle  23753  cmvth  23754  mvth  23755  dvlip  23756  c1liplem1  23759  c1lip1  23760  c1lip2  23761  dveq0  23763  dvgt0lem1  23765  dvgt0lem2  23766  dvgt0  23767  dvlt0  23768  dvge0  23769  dvle  23770  dvivthlem1  23771  dvivth  23773  dvne0  23774  dvne0f1  23775  dvcnvrelem1  23780  dvcnvrelem2  23781  dvcnvre  23782  dvcvx  23783  dvfsumle  23784  dvfsumge  23785  dvfsumabs  23786  ftc1cn  23806  ftc2  23807  ftc2ditglem  23808  ftc2ditg  23809  itgparts  23810  itgsubstlem  23811  itgsubst  23812  ulmcn  24153  psercn  24180  pserdvlem2  24182  pserdv  24183  sincn  24198  coscn  24199  logtayl  24406  dvcncxp1  24484  leibpi  24669  lgamgulmlem2  24756  ftc2re  30676  fdvposlt  30677  fdvneggt  30678  fdvposle  30679  fdvnegge  30680  ivthALT  32330  knoppcld  32495  knoppndv  32525  cnicciblnc  33481  ftc1cnnclem  33483  ftc1cnnc  33484  ftc2nc  33494  cnioobibld  37799  evthiccabs  39718  cncfmptss  39819  mulc1cncfg  39821  expcnfg  39823  mulcncff  40081  cncfshift  40087  subcncff  40093  cncfcompt  40096  addcncff  40097  cncficcgt0  40101  divcncff  40104  cncfiooicclem1  40106  cncfiooiccre  40108  cncfioobd  40110  cncfcompt2  40112  dvsubcncf  40139  dvmulcncf  40140  dvdivcncf  40142  ioodvbdlimc1lem1  40146  cnbdibl  40178  itgsubsticclem  40191  itgsubsticc  40192  itgioocnicc  40193  iblcncfioo  40194  itgiccshift  40196  itgsbtaddcnst  40198  fourierdlem18  40342  fourierdlem32  40356  fourierdlem33  40357  fourierdlem39  40363  fourierdlem48  40371  fourierdlem49  40372  fourierdlem58  40381  fourierdlem59  40382  fourierdlem71  40394  fourierdlem73  40396  fourierdlem81  40404  fourierdlem84  40407  fourierdlem85  40408  fourierdlem88  40411  fourierdlem94  40417  fourierdlem97  40420  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fourierdlem112  40435  fourierdlem113  40436  fouriercn  40449