resco

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

		Ref	Expression
	Assertion	resco	$⊢ {(A \circ B) ↾}_{C} = A \circ ({B ↾}_{C})$

Step	Hyp	Ref	Expression
1		relres	$⊢ Rel ({(A \circ B) ↾}_{C})$
2		relco	$⊢ Rel (A \circ ({B ↾}_{C}))$
3		vex	$⊢ x \in V$
4		vex	$⊢ y \in V$
5	3 4	brco	$⊢ x (A \circ B) y \leftrightarrow \exists z (x B z \land z A y)$
6	5	anbi2i	$⊢ (x \in C \land x (A \circ B) y) \leftrightarrow (x \in C \land \exists z (x B z \land z A y))$
7		19.42v	$⊢ \exists z (x \in C \land (x B z \land z A y)) \leftrightarrow (x \in C \land \exists z (x B z \land z A y))$
8		vex	$⊢ z \in V$
9	8	brresi	$⊢ x ({B ↾}_{C}) z \leftrightarrow (x \in C \land x B z)$
10	9	anbi1i	$⊢ (x ({B ↾}_{C}) z \land z A y) \leftrightarrow ((x \in C \land x B z) \land z A y)$
11		anass	$⊢ ((x \in C \land x B z) \land z A y) \leftrightarrow (x \in C \land (x B z \land z A y))$
12	10 11	bitr2i	$⊢ (x \in C \land (x B z \land z A y)) \leftrightarrow (x ({B ↾}_{C}) z \land z A y)$
13	12	exbii	$⊢ \exists z (x \in C \land (x B z \land z A y)) \leftrightarrow \exists z (x ({B ↾}_{C}) z \land z A y)$
14	6 7 13	3bitr2i	$⊢ (x \in C \land x (A \circ B) y) \leftrightarrow \exists z (x ({B ↾}_{C}) z \land z A y)$
15	4	brresi	$⊢ x ({(A \circ B) ↾}_{C}) y \leftrightarrow (x \in C \land x (A \circ B) y)$
16	3 4	brco	$⊢ x (A \circ ({B ↾}_{C})) y \leftrightarrow \exists z (x ({B ↾}_{C}) z \land z A y)$
17	14 15 16	3bitr4i	$⊢ x ({(A \circ B) ↾}_{C}) y \leftrightarrow x (A \circ ({B ↾}_{C})) y$
18	1 2 17	eqbrriv	$⊢ {(A \circ B) ↾}_{C} = A \circ ({B ↾}_{C})$

Metamath Proof Explorer