Detailed syntax breakdown of Definition df-restrict
Step | Hyp | Ref
| 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 |
7 | 6, 3 | ccom 5572 |
. . . . . 6
class (Range
∘ 1st ) |
8 | 5, 7 | ctxp 33902 |
. . . . 5
class
(2nd ⊗ (Range ∘ 1st
)) |
9 | 4, 8 | ccom 5572 |
. . . 4
class (Cart
∘ (2nd ⊗ (Range ∘ 1st
))) |
10 | 3, 9 | ctxp 33902 |
. . 3
class
(1st ⊗ (Cart ∘ (2nd ⊗ (Range
∘ 1st )))) |
11 | 2, 10 | ccom 5572 |
. 2
class (Cap
∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range
∘ 1st ))))) |
12 | 1, 11 | wceq 1543 |
1
wff Restrict =
(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗
(Range ∘ 1st ))))) |