df-restrict

Description: Define the restriction function. See brrestrict for its value. (Contributed by Scott Fenton, 17-Apr-2014)

		Ref	Expression
	Assertion	df-restrict	$⊢ 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍 = 𝖢𝖺𝗉 \circ (1^{st} \otimes (𝖢𝖺𝗋𝗍 \circ (2^{nd} \otimes (𝖱𝖺𝗇𝗀𝖾 \circ 1^{st}))))$

Step	Hyp	Ref	Expression
0		crestrict	$class 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍$
1		ccap	$class 𝖢𝖺𝗉$
2		c1st	$class 1^{st}$
3		ccart	$class 𝖢𝖺𝗋𝗍$
4		c2nd	$class 2^{nd}$
5		crange	$class 𝖱𝖺𝗇𝗀𝖾$
6	5 2	ccom	$class (𝖱𝖺𝗇𝗀𝖾 \circ 1^{st})$
7	4 6	ctxp	$class (2^{nd} \otimes (𝖱𝖺𝗇𝗀𝖾 \circ 1^{st}))$
8	3 7	ccom	$class (𝖢𝖺𝗋𝗍 \circ (2^{nd} \otimes (𝖱𝖺𝗇𝗀𝖾 \circ 1^{st})))$
9	2 8	ctxp	$class (1^{st} \otimes (𝖢𝖺𝗋𝗍 \circ (2^{nd} \otimes (𝖱𝖺𝗇𝗀𝖾 \circ 1^{st}))))$
10	1 9	ccom	$class (𝖢𝖺𝗉 \circ (1^{st} \otimes (𝖢𝖺𝗋𝗍 \circ (2^{nd} \otimes (𝖱𝖺𝗇𝗀𝖾 \circ 1^{st})))))$
11	0 10	wceq	$wff 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍 = 𝖢𝖺𝗉 \circ (1^{st} \otimes (𝖢𝖺𝗋𝗍 \circ (2^{nd} \otimes (𝖱𝖺𝗇𝗀𝖾 \circ 1^{st}))))$

Metamath Proof Explorer