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 6518 | . . 3 ⊢ (𝜑 → 𝐹 Fn 𝐴) |
3 | off.3 | . . . 4 ⊢ (𝜑 → 𝐺:𝐵⟶𝑇) | |
4 | 3 | ffnd 6518 | . . 3 ⊢ (𝜑 → 𝐺 Fn 𝐵) |
5 | off.4 | . . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
6 | off.5 | . . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑊) | |
7 | off.6 | . . 3 ⊢ (𝐴 ∩ 𝐵) = 𝐶 | |
8 | eqidd 2825 | . . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = (𝐹‘𝑧)) | |
9 | eqidd 2825 | . . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝐺‘𝑧) = (𝐺‘𝑧)) | |
10 | 2, 4, 5, 6, 7, 8, 9 | offval 7419 | . 2 ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑧 ∈ 𝐶 ↦ ((𝐹‘𝑧)𝑅(𝐺‘𝑧)))) |
11 | inss1 4208 | . . . . . 6 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 | |
12 | 7, 11 | eqsstrri 4005 | . . . . 5 ⊢ 𝐶 ⊆ 𝐴 |
13 | 12 | sseli 3966 | . . . 4 ⊢ (𝑧 ∈ 𝐶 → 𝑧 ∈ 𝐴) |
14 | ffvelrn 6852 | . . . 4 ⊢ ((𝐹:𝐴⟶𝑆 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝑆) | |
15 | 1, 13, 14 | syl2an 597 | . . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (𝐹‘𝑧) ∈ 𝑆) |
16 | inss2 4209 | . . . . . 6 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 | |
17 | 7, 16 | eqsstrri 4005 | . . . . 5 ⊢ 𝐶 ⊆ 𝐵 |
18 | 17 | sseli 3966 | . . . 4 ⊢ (𝑧 ∈ 𝐶 → 𝑧 ∈ 𝐵) |
19 | ffvelrn 6852 | . . . 4 ⊢ ((𝐺:𝐵⟶𝑇 ∧ 𝑧 ∈ 𝐵) → (𝐺‘𝑧) ∈ 𝑇) | |
20 | 3, 18, 19 | syl2an 597 | . . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → (𝐺‘𝑧) ∈ 𝑇) |
21 | off.1 | . . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇)) → (𝑥𝑅𝑦) ∈ 𝑈) | |
22 | 21 | ralrimivva 3194 | . . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 (𝑥𝑅𝑦) ∈ 𝑈) |
23 | 22 | adantr 483 | . . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 (𝑥𝑅𝑦) ∈ 𝑈) |
24 | ovrspc2v 7185 | . . 3 ⊢ ((((𝐹‘𝑧) ∈ 𝑆 ∧ (𝐺‘𝑧) ∈ 𝑇) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 (𝑥𝑅𝑦) ∈ 𝑈) → ((𝐹‘𝑧)𝑅(𝐺‘𝑧)) ∈ 𝑈) | |
25 | 15, 20, 23, 24 | syl21anc 835 | . 2 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐶) → ((𝐹‘𝑧)𝑅(𝐺‘𝑧)) ∈ 𝑈) |
26 | 10, 25 | fmpt3d 6883 | 1 ⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺):𝐶⟶𝑈) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1536 ∈ wcel 2113 ∀wral 3141 ∩ cin 3938 ⟶wf 6354 ‘cfv 6358 (class class class)co 7159 ∘f cof 7410 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-rep 5193 ax-sep 5206 ax-nul 5213 ax-pr 5333 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ne 3020 df-ral 3146 df-rex 3147 df-reu 3148 df-rab 3150 df-v 3499 df-sbc 3776 df-csb 3887 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-nul 4295 df-if 4471 df-sn 4571 df-pr 4573 df-op 4577 df-uni 4842 df-iun 4924 df-br 5070 df-opab 5132 df-mpt 5150 df-id 5463 df-xp 5564 df-rel 5565 df-cnv 5566 df-co 5567 df-dm 5568 df-rn 5569 df-res 5570 df-ima 5571 df-iota 6317 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-ov 7162 df-oprab 7163 df-mpo 7164 df-of 7412 |
This theorem is referenced by: suppofssd 7870 o1of2 14972 ghmplusg 18969 gsumzaddlem 19044 gsumzadd 19045 lcomf 19676 psrbagaddcl 20153 psraddcl 20166 psrvscacl 20176 psrbagev1 20293 evlslem3 20296 frlmup1 20945 mndvcl 21005 tsmsadd 22758 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 24538 dvmulbr 24539 dvaddf 24542 dvmulf 24543 dv11cn 24601 plyaddlem 24808 coeeulem 24817 coeaddlem 24842 plydivlem4 24888 jensenlem2 25568 jensen 25569 basellem7 25667 basellem9 25669 dchrmulcl 25828 ofrn 30389 offinsupp1 30466 fedgmullem1 31029 sibfof 31602 signshf 31862 circlemethhgt 31918 poimirlem23 34919 poimirlem24 34920 poimirlem25 34921 poimirlem29 34925 poimirlem30 34926 poimirlem31 34927 poimirlem32 34928 itg2addnc 34950 ftc1anclem3 34973 ftc1anclem6 34976 ftc1anclem8 34978 lfladdcl 36211 lflvscl 36217 mzpclall 39330 mzpindd 39349 expgrowth 40673 binomcxplemnotnn0 40694 dvdivcncf 42218 ofaddmndmap 44399 amgmwlem 44910 |
Copyright terms: Public domain | W3C validator |