![]() |
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 6737 | . . 3 ⊢ (𝜑 → 𝐹 Fn 𝐴) |
3 | off.3 | . . . 4 ⊢ (𝜑 → 𝐺:𝐵⟶𝑇) | |
4 | 3 | ffnd 6737 | . . 3 ⊢ (𝜑 → 𝐺 Fn 𝐵) |
5 | off.4 | . . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
6 | off.5 | . . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑊) | |
7 | off.6 | . . 3 ⊢ (𝐴 ∩ 𝐵) = 𝐶 | |
8 | eqidd 2735 | . . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = (𝐹‘𝑧)) | |
9 | eqidd 2735 | . . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐺‘𝑧) = (𝐺‘𝑧)) | |
10 | 2, 4, 5, 6, 7, 8, 9 | offval 7705 | . 2 ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑧 ∈ 𝐶 ↦ ((𝐹‘𝑧)𝑅(𝐺‘𝑧)))) |
11 | inss1 4244 | . . . . . 6 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 | |
12 | 7, 11 | eqsstrri 4030 | . . . . 5 ⊢ 𝐶 ⊆ 𝐴 |
13 | 12 | sseli 3990 | . . . 4 ⊢ (𝑧 ∈ 𝐶 → 𝑧 ∈ 𝐴) |
14 | ffvelcdm 7100 | . . . 4 ⊢ ((𝐹:𝐴⟶𝑆 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝑆) | |
15 | 1, 13, 14 | syl2an 596 | . . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (𝐹‘𝑧) ∈ 𝑆) |
16 | inss2 4245 | . . . . . 6 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 | |
17 | 7, 16 | eqsstrri 4030 | . . . . 5 ⊢ 𝐶 ⊆ 𝐵 |
18 | 17 | sseli 3990 | . . . 4 ⊢ (𝑧 ∈ 𝐶 → 𝑧 ∈ 𝐵) |
19 | ffvelcdm 7100 | . . . 4 ⊢ ((𝐺:𝐵⟶𝑇 ∧ 𝑧 ∈ 𝐵) → (𝐺‘𝑧) ∈ 𝑇) | |
20 | 3, 18, 19 | syl2an 596 | . . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (𝐺‘𝑧) ∈ 𝑇) |
21 | off.1 | . . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈) | |
22 | 21 | ralrimivva 3199 | . . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 (𝑥𝑅𝑦) ∈ 𝑈) |
23 | 22 | adantr 480 | . . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 (𝑥𝑅𝑦) ∈ 𝑈) |
24 | ovrspc2v 7456 | . . 3 ⊢ ((((𝐹‘𝑧) ∈ 𝑆 ∧ (𝐺‘𝑧) ∈ 𝑇) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 (𝑥𝑅𝑦) ∈ 𝑈) → ((𝐹‘𝑧)𝑅(𝐺‘𝑧)) ∈ 𝑈) | |
25 | 15, 20, 23, 24 | syl21anc 838 | . 2 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐹‘𝑧)𝑅(𝐺‘𝑧)) ∈ 𝑈) |
26 | 10, 25 | fmpt3d 7135 | 1 ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺):𝐶⟶𝑈) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1536 ∈ wcel 2105 ∀wral 3058 ∩ cin 3961 ⟶wf 6558 ‘cfv 6562 (class class class)co 7430 ∘f cof 7694 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-rep 5284 ax-sep 5301 ax-nul 5311 ax-pr 5437 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-ral 3059 df-rex 3068 df-reu 3378 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-iun 4997 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5582 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570 df-ov 7433 df-oprab 7434 df-mpo 7435 df-of 7696 |
This theorem is referenced by: suppofssd 8226 o1of2 15645 mndvcl 18822 ghmplusg 19878 gsumzaddlem 19953 gsumzadd 19954 lcomf 20915 frlmup1 21835 psrbagaddcl 21961 psraddcl 21975 psraddclOLD 21976 psrvscacl 21988 psrbagev1 22118 evlslem3 22121 tsmsadd 24170 mbfmulc2lem 25695 mbfaddlem 25708 i1fadd 25743 i1fmul 25744 itg1addlem4 25747 itg1addlem4OLD 25748 i1fmulclem 25751 i1fmulc 25752 mbfi1flimlem 25771 itg2mulclem 25795 itg2mulc 25796 itg2monolem1 25799 itg2addlem 25807 dvaddbr 25988 dvmulbr 25989 dvmulbrOLD 25990 dvaddf 25993 dvmulf 25994 dv11cn 26054 plyaddlem 26268 coeeulem 26277 coeaddlem 26302 plydivlem4 26352 jensenlem2 27045 jensen 27046 basellem7 27144 basellem9 27146 dchrmulcl 27307 ofrn 32655 offinsupp1 32744 elrgspnlem1 33231 1arithidomlem2 33543 1arithidom 33544 ply1degltdimlem 33649 fedgmullem1 33656 sibfof 34321 signshf 34581 circlemethhgt 34636 poimirlem23 37629 poimirlem24 37630 poimirlem25 37631 poimirlem29 37635 poimirlem30 37636 poimirlem31 37637 poimirlem32 37638 itg2addnc 37660 ftc1anclem3 37681 ftc1anclem6 37684 ftc1anclem8 37686 lfladdcl 39052 lflvscl 39058 fsuppssind 42579 mhphf 42583 mzpclall 42714 mzpindd 42733 expgrowth 44330 binomcxplemnotnn0 44351 dvdivcncf 45882 ofaddmndmap 48187 amgmwlem 49032 |
Copyright terms: Public domain | W3C validator |