Metamath Proof Explorer

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 o. ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 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 o. 1st )
7 4 6 ctxp 
 |-  ( 2nd (x) ( Range o. 1st ) )
8 3 7 ccom 
 |-  ( Cart o. ( 2nd (x) ( Range o. 1st ) ) )
9 2 8 ctxp 
 |-  ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) )
10 1 9 ccom 
 |-  ( Cap o. ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) ) )
11 0 10 wceq 
 |-  Restrict = ( Cap o. ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) ) )