![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cores | Structured version Visualization version GIF version |
Description: Restricted first member of a class composition. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Ref | Expression |
---|---|
cores | ⊢ (ran 𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ∘ 𝐵) = (𝐴 ∘ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3482 | . . . . . . 7 ⊢ 𝑧 ∈ V | |
2 | vex 3482 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
3 | 1, 2 | brelrn 5956 | . . . . . 6 ⊢ (𝑧𝐵𝑦 → 𝑦 ∈ ran 𝐵) |
4 | ssel 3989 | . . . . . 6 ⊢ (ran 𝐵 ⊆ 𝐶 → (𝑦 ∈ ran 𝐵 → 𝑦 ∈ 𝐶)) | |
5 | vex 3482 | . . . . . . . 8 ⊢ 𝑥 ∈ V | |
6 | 5 | brresi 6009 | . . . . . . 7 ⊢ (𝑦(𝐴 ↾ 𝐶)𝑥 ↔ (𝑦 ∈ 𝐶 ∧ 𝑦𝐴𝑥)) |
7 | 6 | baib 535 | . . . . . 6 ⊢ (𝑦 ∈ 𝐶 → (𝑦(𝐴 ↾ 𝐶)𝑥 ↔ 𝑦𝐴𝑥)) |
8 | 3, 4, 7 | syl56 36 | . . . . 5 ⊢ (ran 𝐵 ⊆ 𝐶 → (𝑧𝐵𝑦 → (𝑦(𝐴 ↾ 𝐶)𝑥 ↔ 𝑦𝐴𝑥))) |
9 | 8 | pm5.32d 577 | . . . 4 ⊢ (ran 𝐵 ⊆ 𝐶 → ((𝑧𝐵𝑦 ∧ 𝑦(𝐴 ↾ 𝐶)𝑥) ↔ (𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥))) |
10 | 9 | exbidv 1919 | . . 3 ⊢ (ran 𝐵 ⊆ 𝐶 → (∃𝑦(𝑧𝐵𝑦 ∧ 𝑦(𝐴 ↾ 𝐶)𝑥) ↔ ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥))) |
11 | 10 | opabbidv 5214 | . 2 ⊢ (ran 𝐵 ⊆ 𝐶 → {〈𝑧, 𝑥〉 ∣ ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦(𝐴 ↾ 𝐶)𝑥)} = {〈𝑧, 𝑥〉 ∣ ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)}) |
12 | df-co 5698 | . 2 ⊢ ((𝐴 ↾ 𝐶) ∘ 𝐵) = {〈𝑧, 𝑥〉 ∣ ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦(𝐴 ↾ 𝐶)𝑥)} | |
13 | df-co 5698 | . 2 ⊢ (𝐴 ∘ 𝐵) = {〈𝑧, 𝑥〉 ∣ ∃𝑦(𝑧𝐵𝑦 ∧ 𝑦𝐴𝑥)} | |
14 | 11, 12, 13 | 3eqtr4g 2800 | 1 ⊢ (ran 𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ∘ 𝐵) = (𝐴 ∘ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1537 ∃wex 1776 ∈ wcel 2106 ⊆ wss 3963 class class class wbr 5148 {copab 5210 ran crn 5690 ↾ cres 5691 ∘ ccom 5693 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pr 5438 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-ral 3060 df-rex 3069 df-rab 3434 df-v 3480 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-nul 4340 df-if 4532 df-sn 4632 df-pr 4634 df-op 4638 df-br 5149 df-opab 5211 df-xp 5695 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 |
This theorem is referenced by: cocnvcnv1 6279 cores2 6281 relcoi2 6299 funresfunco 6609 fco2 6763 fcoi2 6784 f1ocoima 7323 domss2 9175 cottrcl 9757 canthp1lem2 10691 imasdsval2 17563 frmdss2 18889 gsumval3lem1 19938 gsumzres 19942 gsumzaddlem 19954 dprdf1 20068 kgencn2 23581 tsmsf1o 24169 lgamcvg2 27113 hhssims 31303 ccatws1f1olast 32922 symgcom 33086 cycpmconjslem1 33157 cycpmconjslem2 33158 eulerpartgbij 34354 cvmlift2lem9a 35288 poimirlem9 37616 fourierdlem53 46115 |
Copyright terms: Public domain | W3C validator |