df-restrict - Mathbox for Scott Fenton

	Mathbox for Scott Fenton		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-restrict		Structured version Visualization version GIF version

Definition df-restrict 36183

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

**Assertion**
Ref	Expression
df-restrict	⊢ Restrict = (Cap ∘ (1^st ⊗ (Cart ∘ (2^nd ⊗ (Range ∘ 1^st )))))

**Detailed syntax breakdown of Definition df-restrict**
Step	Hyp	Ref	Expression
1		crestrict 36163	. 2 class Restrict
2		ccap 36159	. . 3 class Cap
3		c1st 7964	. . . 4 class 1^st
4		ccart 36153	. . . . 5 class Cart
5		c2nd 7965	. . . . . 6 class 2^nd
6		crange 36156	. . . . . . 7 class Range
7	6, 3	ccom 5649	. . . . . 6 class (Range ∘ 1^st )
8	5, 7	ctxp 36142	. . . . 5 class (2^nd ⊗ (Range ∘ 1^st ))
9	4, 8	ccom 5649	. . . 4 class (Cart ∘ (2^nd ⊗ (Range ∘ 1^st )))
10	3, 9	ctxp 36142	. . 3 class (1^st ⊗ (Cart ∘ (2^nd ⊗ (Range ∘ 1^st ))))
11	2, 10	ccom 5649	. 2 class (Cap ∘ (1^st ⊗ (Cart ∘ (2^nd ⊗ (Range ∘ 1^st )))))
12	1, 11	wceq 1559	1 wff Restrict = (Cap ∘ (1^st ⊗ (Cart ∘ (2^nd ⊗ (Range ∘ 1^st )))))

Colors of variables: wff setvar class

This definition is referenced by: brrestrict 36263