Definition df-restrict

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

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

Detailed syntax breakdown

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