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	⊢ Restrict = ( Cap ∘ ( 1st ⊗ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crestrict	⊢ Restrict
1		ccap	⊢ Cap
2		c1st	⊢ 1st
3		ccart	⊢ Cart
4		c2nd	⊢ 2nd
5		crange	⊢ Range
6	5 2	ccom	⊢ ( Range ∘ 1st )
7	4 6	ctxp	⊢ ( 2nd ⊗ ( Range ∘ 1st ) )
8	3 7	ccom	⊢ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) )
9	2 8	ctxp	⊢ ( 1st ⊗ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) )
10	1 9	ccom	⊢ ( Cap ∘ ( 1st ⊗ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) ) )
11	0 10	wceq	⊢ Restrict = ( Cap ∘ ( 1st ⊗ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) ) )