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 31147
 Description: Define the restriction function. See brrestrict 31226 for its value. (Contributed by Scott Fenton, 17-Apr-2014.)
Assertion
Ref Expression
df-restrict Restrict = (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))

Detailed syntax breakdown of Definition df-restrict
StepHypRef Expression
1 crestrict 31127 . 2 class Restrict
2 ccap 31123 . . 3 class Cap
3 c1st 7057 . . . 4 class 1st
4 ccart 31117 . . . . 5 class Cart
5 c2nd 7058 . . . . . 6 class 2nd
6 crange 31120 . . . . . . 7 class Range
76, 3ccom 5042 . . . . . 6 class (Range ∘ 1st )
85, 7ctxp 31106 . . . . 5 class (2nd ⊗ (Range ∘ 1st ))
94, 8ccom 5042 . . . 4 class (Cart ∘ (2nd ⊗ (Range ∘ 1st )))
103, 9ctxp 31106 . . 3 class (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))
112, 10ccom 5042 . 2 class (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))
121, 11wceq 1475 1 wff Restrict = (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))
 Colors of variables: wff setvar class This definition is referenced by:  brrestrict  31226
 Copyright terms: Public domain W3C validator