![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > resco | Structured version Visualization version GIF version |
Description: Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006.) |
Ref | Expression |
---|---|
resco | ⊢ ((𝐴 ∘ 𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵 ↾ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relres 5971 | . 2 ⊢ Rel ((𝐴 ∘ 𝐵) ↾ 𝐶) | |
2 | relco 6065 | . 2 ⊢ Rel (𝐴 ∘ (𝐵 ↾ 𝐶)) | |
3 | vex 3452 | . . . . . 6 ⊢ 𝑥 ∈ V | |
4 | vex 3452 | . . . . . 6 ⊢ 𝑦 ∈ V | |
5 | 3, 4 | brco 5831 | . . . . 5 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)) |
6 | 5 | anbi2i 624 | . . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑥(𝐴 ∘ 𝐵)𝑦) ↔ (𝑥 ∈ 𝐶 ∧ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦))) |
7 | 19.42v 1958 | . . . 4 ⊢ (∃𝑧(𝑥 ∈ 𝐶 ∧ (𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)) ↔ (𝑥 ∈ 𝐶 ∧ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦))) | |
8 | vex 3452 | . . . . . . . 8 ⊢ 𝑧 ∈ V | |
9 | 8 | brresi 5951 | . . . . . . 7 ⊢ (𝑥(𝐵 ↾ 𝐶)𝑧 ↔ (𝑥 ∈ 𝐶 ∧ 𝑥𝐵𝑧)) |
10 | 9 | anbi1i 625 | . . . . . 6 ⊢ ((𝑥(𝐵 ↾ 𝐶)𝑧 ∧ 𝑧𝐴𝑦) ↔ ((𝑥 ∈ 𝐶 ∧ 𝑥𝐵𝑧) ∧ 𝑧𝐴𝑦)) |
11 | anass 470 | . . . . . 6 ⊢ (((𝑥 ∈ 𝐶 ∧ 𝑥𝐵𝑧) ∧ 𝑧𝐴𝑦) ↔ (𝑥 ∈ 𝐶 ∧ (𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦))) | |
12 | 10, 11 | bitr2i 276 | . . . . 5 ⊢ ((𝑥 ∈ 𝐶 ∧ (𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)) ↔ (𝑥(𝐵 ↾ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)) |
13 | 12 | exbii 1851 | . . . 4 ⊢ (∃𝑧(𝑥 ∈ 𝐶 ∧ (𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)) ↔ ∃𝑧(𝑥(𝐵 ↾ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)) |
14 | 6, 7, 13 | 3bitr2i 299 | . . 3 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑥(𝐴 ∘ 𝐵)𝑦) ↔ ∃𝑧(𝑥(𝐵 ↾ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)) |
15 | 4 | brresi 5951 | . . 3 ⊢ (𝑥((𝐴 ∘ 𝐵) ↾ 𝐶)𝑦 ↔ (𝑥 ∈ 𝐶 ∧ 𝑥(𝐴 ∘ 𝐵)𝑦)) |
16 | 3, 4 | brco 5831 | . . 3 ⊢ (𝑥(𝐴 ∘ (𝐵 ↾ 𝐶))𝑦 ↔ ∃𝑧(𝑥(𝐵 ↾ 𝐶)𝑧 ∧ 𝑧𝐴𝑦)) |
17 | 14, 15, 16 | 3bitr4i 303 | . 2 ⊢ (𝑥((𝐴 ∘ 𝐵) ↾ 𝐶)𝑦 ↔ 𝑥(𝐴 ∘ (𝐵 ↾ 𝐶))𝑦) |
18 | 1, 2, 17 | eqbrriv 5752 | 1 ⊢ ((𝐴 ∘ 𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵 ↾ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 397 = wceq 1542 ∃wex 1782 ∈ wcel 2107 class class class wbr 5110 ↾ cres 5640 ∘ ccom 5642 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 ax-sep 5261 ax-nul 5268 ax-pr 5389 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-ral 3066 df-rex 3075 df-rab 3411 df-v 3450 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-if 4492 df-sn 4592 df-pr 4594 df-op 4598 df-br 5111 df-opab 5173 df-xp 5644 df-rel 5645 df-co 5647 df-res 5650 |
This theorem is referenced by: cocnvcnv2 6215 coires1 6221 dftpos2 8179 ttrclco 9661 canthp1lem2 10596 o1res 15449 gsumzaddlem 19705 tsmsf1o 23512 tsmsmhm 23513 mbfres 25024 hhssims 30258 symgcom 31976 cycpmconjslem1 32045 cycpmconjslem2 32046 erdsze2lem2 33838 cvmlift2lem9a 33937 mbfresfi 36153 cocnv 36213 xrnres 36893 xrnres2 36894 xrnres3 36895 diophrw 41111 eldioph2 41114 mbfres2cn 44273 funcoressn 45350 |
Copyright terms: Public domain | W3C validator |