Mathbox for Glauco Siliprandi |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > cncfmptssg | Structured version Visualization version GIF version |
Description: A continuous complex function restricted to a subset is continuous, using maps-to notation. This theorem generalizes cncfmptss 42757 because it allows to establish a subset for the codomain also. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Ref | Expression |
---|---|
cncfmptssg.2 | ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐸) |
cncfmptssg.3 | ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵)) |
cncfmptssg.4 | ⊢ (𝜑 → 𝐶 ⊆ 𝐴) |
cncfmptssg.5 | ⊢ (𝜑 → 𝐷 ⊆ 𝐵) |
cncfmptssg.6 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐸 ∈ 𝐷) |
Ref | Expression |
---|---|
cncfmptssg | ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐸) ∈ (𝐶–cn→𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cncfmptssg.6 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐸 ∈ 𝐷) | |
2 | 1 | fmpttd 6921 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐸):𝐶⟶𝐷) |
3 | cncfmptssg.5 | . . . 4 ⊢ (𝜑 → 𝐷 ⊆ 𝐵) | |
4 | cncfmptssg.3 | . . . . 5 ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵)) | |
5 | cncfrss2 23761 | . . . . 5 ⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ) | |
6 | 4, 5 | syl 17 | . . . 4 ⊢ (𝜑 → 𝐵 ⊆ ℂ) |
7 | 3, 6 | sstrd 3901 | . . 3 ⊢ (𝜑 → 𝐷 ⊆ ℂ) |
8 | cncfmptssg.4 | . . . . . . 7 ⊢ (𝜑 → 𝐶 ⊆ 𝐴) | |
9 | 8 | sselda 3891 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐴) |
10 | cncfmptssg.2 | . . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐸) | |
11 | 10 | fvmpt2 6818 | . . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐸 ∈ 𝐷) → (𝐹‘𝑥) = 𝐸) |
12 | 9, 1, 11 | syl2anc 587 | . . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) = 𝐸) |
13 | 12 | mpteq2dva 5139 | . . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ 𝐸)) |
14 | nfmpt1 5142 | . . . . . 6 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐸) | |
15 | 10, 14 | nfcxfr 2898 | . . . . 5 ⊢ Ⅎ𝑥𝐹 |
16 | 15, 4, 8 | cncfmptss 42757 | . . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ (𝐶–cn→𝐵)) |
17 | 13, 16 | eqeltrrd 2835 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐸) ∈ (𝐶–cn→𝐵)) |
18 | cncffvrn 23767 | . . 3 ⊢ ((𝐷 ⊆ ℂ ∧ (𝑥 ∈ 𝐶 ↦ 𝐸) ∈ (𝐶–cn→𝐵)) → ((𝑥 ∈ 𝐶 ↦ 𝐸) ∈ (𝐶–cn→𝐷) ↔ (𝑥 ∈ 𝐶 ↦ 𝐸):𝐶⟶𝐷)) | |
19 | 7, 17, 18 | syl2anc 587 | . 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐶 ↦ 𝐸) ∈ (𝐶–cn→𝐷) ↔ (𝑥 ∈ 𝐶 ↦ 𝐸):𝐶⟶𝐷)) |
20 | 2, 19 | mpbird 260 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ 𝐸) ∈ (𝐶–cn→𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1543 ∈ wcel 2110 ⊆ wss 3857 ↦ cmpt 5124 ⟶wf 6365 ‘cfv 6369 (class class class)co 7202 ℂcc 10710 –cn→ccncf 23745 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2706 ax-sep 5181 ax-nul 5188 ax-pow 5247 ax-pr 5311 ax-un 7512 ax-cnex 10768 ax-resscn 10769 ax-1cn 10770 ax-icn 10771 ax-addcl 10772 ax-addrcl 10773 ax-mulcl 10774 ax-mulrcl 10775 ax-mulcom 10776 ax-addass 10777 ax-mulass 10778 ax-distr 10779 ax-i2m1 10780 ax-1ne0 10781 ax-1rid 10782 ax-rnegex 10783 ax-rrecex 10784 ax-cnre 10785 ax-pre-lttri 10786 ax-pre-lttrn 10787 ax-pre-ltadd 10788 ax-pre-mulgt0 10789 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2726 df-clel 2812 df-nfc 2882 df-ne 2936 df-nel 3040 df-ral 3059 df-rex 3060 df-reu 3061 df-rmo 3062 df-rab 3063 df-v 3403 df-sbc 3688 df-csb 3803 df-dif 3860 df-un 3862 df-in 3864 df-ss 3874 df-nul 4228 df-if 4430 df-pw 4505 df-sn 4532 df-pr 4534 df-op 4538 df-uni 4810 df-br 5044 df-opab 5106 df-mpt 5125 df-id 5444 df-po 5457 df-so 5458 df-xp 5546 df-rel 5547 df-cnv 5548 df-co 5549 df-dm 5550 df-rn 5551 df-res 5552 df-ima 5553 df-iota 6327 df-fun 6371 df-fn 6372 df-f 6373 df-f1 6374 df-fo 6375 df-f1o 6376 df-fv 6377 df-riota 7159 df-ov 7205 df-oprab 7206 df-mpo 7207 df-er 8380 df-map 8499 df-en 8616 df-dom 8617 df-sdom 8618 df-pnf 10852 df-mnf 10853 df-xr 10854 df-ltxr 10855 df-le 10856 df-sub 11047 df-neg 11048 df-div 11473 df-2 11876 df-cj 14645 df-re 14646 df-im 14647 df-abs 14782 df-cncf 23747 |
This theorem is referenced by: negcncfg 43051 itgsinexplem1 43124 itgiccshift 43150 itgperiod 43151 itgsbtaddcnst 43152 dirkeritg 43272 dirkercncflem2 43274 dirkercncflem4 43276 fourierdlem18 43295 fourierdlem23 43300 fourierdlem39 43316 fourierdlem40 43317 fourierdlem62 43338 fourierdlem73 43349 fourierdlem78 43354 fourierdlem83 43359 fourierdlem84 43360 fourierdlem93 43369 fourierdlem95 43371 fourierdlem101 43377 fourierdlem111 43387 etransclem46 43450 |
Copyright terms: Public domain | W3C validator |