Users' Mathboxes 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 33943
Description: Define the restriction function. See brrestrict 34021 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 33923 . 2 class Restrict
2 ccap 33919 . . 3 class Cap
3 c1st 7780 . . . 4 class 1st
4 ccart 33913 . . . . 5 class Cart
5 c2nd 7781 . . . . . 6 class 2nd
6 crange 33916 . . . . . . 7 class Range
76, 3ccom 5572 . . . . . 6 class (Range ∘ 1st )
85, 7ctxp 33902 . . . . 5 class (2nd ⊗ (Range ∘ 1st ))
94, 8ccom 5572 . . . 4 class (Cart ∘ (2nd ⊗ (Range ∘ 1st )))
103, 9ctxp 33902 . . 3 class (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))
112, 10ccom 5572 . 2 class (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))
121, 11wceq 1543 1 wff Restrict = (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))
Colors of variables: wff setvar class
This definition is referenced by:  brrestrict  34021
  Copyright terms: Public domain W3C validator