![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > off | Structured version Visualization version GIF version |
Description: The function operation produces a function. (Contributed by Mario Carneiro, 20-Jul-2014.) |
Ref | Expression |
---|---|
off.1 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈) |
off.2 | ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) |
off.3 | ⊢ (𝜑 → 𝐺:𝐵⟶𝑇) |
off.4 | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
off.5 | ⊢ (𝜑 → 𝐵 ∈ 𝑊) |
off.6 | ⊢ (𝐴 ∩ 𝐵) = 𝐶 |
Ref | Expression |
---|---|
off | ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺):𝐶⟶𝑈) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | off.2 | . . . 4 ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) | |
2 | 1 | ffnd 6488 | . . 3 ⊢ (𝜑 → 𝐹 Fn 𝐴) |
3 | off.3 | . . . 4 ⊢ (𝜑 → 𝐺:𝐵⟶𝑇) | |
4 | 3 | ffnd 6488 | . . 3 ⊢ (𝜑 → 𝐺 Fn 𝐵) |
5 | off.4 | . . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
6 | off.5 | . . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑊) | |
7 | off.6 | . . 3 ⊢ (𝐴 ∩ 𝐵) = 𝐶 | |
8 | eqidd 2799 | . . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = (𝐹‘𝑧)) | |
9 | eqidd 2799 | . . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐺‘𝑧) = (𝐺‘𝑧)) | |
10 | 2, 4, 5, 6, 7, 8, 9 | offval 7396 | . 2 ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑧 ∈ 𝐶 ↦ ((𝐹‘𝑧)𝑅(𝐺‘𝑧)))) |
11 | inss1 4155 | . . . . . 6 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 | |
12 | 7, 11 | eqsstrri 3950 | . . . . 5 ⊢ 𝐶 ⊆ 𝐴 |
13 | 12 | sseli 3911 | . . . 4 ⊢ (𝑧 ∈ 𝐶 → 𝑧 ∈ 𝐴) |
14 | ffvelrn 6826 | . . . 4 ⊢ ((𝐹:𝐴⟶𝑆 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝑆) | |
15 | 1, 13, 14 | syl2an 598 | . . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (𝐹‘𝑧) ∈ 𝑆) |
16 | inss2 4156 | . . . . . 6 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 | |
17 | 7, 16 | eqsstrri 3950 | . . . . 5 ⊢ 𝐶 ⊆ 𝐵 |
18 | 17 | sseli 3911 | . . . 4 ⊢ (𝑧 ∈ 𝐶 → 𝑧 ∈ 𝐵) |
19 | ffvelrn 6826 | . . . 4 ⊢ ((𝐺:𝐵⟶𝑇 ∧ 𝑧 ∈ 𝐵) → (𝐺‘𝑧) ∈ 𝑇) | |
20 | 3, 18, 19 | syl2an 598 | . . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (𝐺‘𝑧) ∈ 𝑇) |
21 | off.1 | . . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈) | |
22 | 21 | ralrimivva 3156 | . . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 (𝑥𝑅𝑦) ∈ 𝑈) |
23 | 22 | adantr 484 | . . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 (𝑥𝑅𝑦) ∈ 𝑈) |
24 | ovrspc2v 7161 | . . 3 ⊢ ((((𝐹‘𝑧) ∈ 𝑆 ∧ (𝐺‘𝑧) ∈ 𝑇) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 (𝑥𝑅𝑦) ∈ 𝑈) → ((𝐹‘𝑧)𝑅(𝐺‘𝑧)) ∈ 𝑈) | |
25 | 15, 20, 23, 24 | syl21anc 836 | . 2 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐹‘𝑧)𝑅(𝐺‘𝑧)) ∈ 𝑈) |
26 | 10, 25 | fmpt3d 6857 | 1 ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺):𝐶⟶𝑈) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1538 ∈ wcel 2111 ∀wral 3106 ∩ cin 3880 ⟶wf 6320 ‘cfv 6324 (class class class)co 7135 ∘f cof 7387 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-reu 3113 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-ov 7138 df-oprab 7139 df-mpo 7140 df-of 7389 |
This theorem is referenced by: suppofssd 7850 o1of2 14961 ghmplusg 18959 gsumzaddlem 19034 gsumzadd 19035 lcomf 19666 frlmup1 20487 psrbagaddcl 20608 psraddcl 20621 psrvscacl 20631 psrbagev1 20749 evlslem3 20752 mndvcl 20998 tsmsadd 22752 mbfmulc2lem 24251 mbfaddlem 24264 i1fadd 24299 i1fmul 24300 itg1addlem4 24303 i1fmulclem 24306 i1fmulc 24307 mbfi1flimlem 24326 itg2mulclem 24350 itg2mulc 24351 itg2monolem1 24354 itg2addlem 24362 dvaddbr 24541 dvmulbr 24542 dvaddf 24545 dvmulf 24546 dv11cn 24604 plyaddlem 24812 coeeulem 24821 coeaddlem 24846 plydivlem4 24892 jensenlem2 25573 jensen 25574 basellem7 25672 basellem9 25674 dchrmulcl 25833 ofrn 30400 offinsupp1 30489 fedgmullem1 31113 sibfof 31708 signshf 31968 circlemethhgt 32024 poimirlem23 35080 poimirlem24 35081 poimirlem25 35082 poimirlem29 35086 poimirlem30 35087 poimirlem31 35088 poimirlem32 35089 itg2addnc 35111 ftc1anclem3 35132 ftc1anclem6 35135 ftc1anclem8 35137 lfladdcl 36367 lflvscl 36373 fsuppssind 39459 mzpclall 39668 mzpindd 39687 expgrowth 41039 binomcxplemnotnn0 41060 dvdivcncf 42569 ofaddmndmap 44745 amgmwlem 45330 |
Copyright terms: Public domain | W3C validator |