Theorem resco 6248

Description: Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006.)

Assertion

Ref	Expression
resco	⊢ ((𝐴 ∘ 𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵 ↾ 𝐶))

Proof of Theorem resco

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relres 6008	. 2 ⊢ Rel ((𝐴 ∘ 𝐵) ↾ 𝐶)
2		relco 6106	. 2 ⊢ Rel (𝐴 ∘ (𝐵 ↾ 𝐶))
3		vex 3473	. . . . . 6 ⊢ 𝑥 ∈ V
4		vex 3473	. . . . . 6 ⊢ 𝑦 ∈ V
5	3, 4	brco 5867	. . . . 5 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦))
6	5	anbi2i 622	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑥(𝐴 ∘ 𝐵)𝑦) ↔ (𝑥 ∈ 𝐶 ∧ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)))
7		19.42v 1950	. . . 4 ⊢ (∃𝑧(𝑥 ∈ 𝐶 ∧ (𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)) ↔ (𝑥 ∈ 𝐶 ∧ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)))
8		vex 3473	. . . . . . . 8 ⊢ 𝑧 ∈ V
9	8	brresi 5988	. . . . . . 7 ⊢ (𝑥(𝐵 ↾ 𝐶)𝑧 ↔ (𝑥 ∈ 𝐶 ∧ 𝑥𝐵𝑧))
10	9	anbi1i 623	. . . . . 6 ⊢ ((𝑥(𝐵 ↾ 𝐶)𝑧 ∧ 𝑧𝐴𝑦) ↔ ((𝑥 ∈ 𝐶 ∧ 𝑥𝐵𝑧) ∧ 𝑧𝐴𝑦))
11		anass 468	. . . . . 6 ⊢ (((𝑥 ∈ 𝐶 ∧ 𝑥𝐵𝑧) ∧ 𝑧𝐴𝑦) ↔ (𝑥 ∈ 𝐶 ∧ (𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)))
12	10, 11	bitr2i 276	. . . . 5 ⊢ ((𝑥 ∈ 𝐶 ∧ (𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)) ↔ (𝑥(𝐵 ↾ 𝐶)𝑧 ∧ 𝑧𝐴𝑦))
13	12	exbii 1843	. . . 4 ⊢ (∃𝑧(𝑥 ∈ 𝐶 ∧ (𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)) ↔ ∃𝑧(𝑥(𝐵 ↾ 𝐶)𝑧 ∧ 𝑧𝐴𝑦))
14	6, 7, 13	3bitr2i 299	. . 3 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑥(𝐴 ∘ 𝐵)𝑦) ↔ ∃𝑧(𝑥(𝐵 ↾ 𝐶)𝑧 ∧ 𝑧𝐴𝑦))
15	4	brresi 5988	. . 3 ⊢ (𝑥((𝐴 ∘ 𝐵) ↾ 𝐶)𝑦 ↔ (𝑥 ∈ 𝐶 ∧ 𝑥(𝐴 ∘ 𝐵)𝑦))
16	3, 4	brco 5867	. . 3 ⊢ (𝑥(𝐴 ∘ (𝐵 ↾ 𝐶))𝑦 ↔ ∃𝑧(𝑥(𝐵 ↾ 𝐶)𝑧 ∧ 𝑧𝐴𝑦))
17	14, 15, 16	3bitr4i 303	. 2 ⊢ (𝑥((𝐴 ∘ 𝐵) ↾ 𝐶)𝑦 ↔ 𝑥(𝐴 ∘ (𝐵 ↾ 𝐶))𝑦)
18	1, 2, 17	eqbrriv 5787	1 ⊢ ((𝐴 ∘ 𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵 ↾ 𝐶))

Syntax hints:   ∧ wa 395   = wceq 1534  ∃wex 1774   ∈ wcel 2099   class class class wbr 5142   ↾ cres 5674   ∘ ccom 5676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5143  df-opab 5205  df-xp 5678  df-rel 5679  df-co 5681  df-res 5684

This theorem is referenced by:  cocnvcnv2  6256  coires1  6262  dftpos2  8242  ttrclco  9733  canthp1lem2  10668  o1res  15528  gsumzaddlem  19867  tsmsf1o  24036  tsmsmhm  24037  mbfres  25560  hhssims  31071  symgcom  32784  cycpmconjslem1  32853  cycpmconjslem2  32854  erdsze2lem2  34750  cvmlift2lem9a  34849  mbfresfi  37074  cocnv  37133  xrnres  37811  xrnres2  37812  xrnres3  37813  diophrw  42101  eldioph2  42104  mbfres2cn  45269  funcoressn  46347