Detailed syntax breakdown of Definition df-resc
Step | Hyp | Ref
| Expression |
1 | | cresc 17520 |
. 2
class
↾cat |
2 | | vc |
. . 3
setvar 𝑐 |
3 | | vh |
. . 3
setvar ℎ |
4 | | cvv 3432 |
. . 3
class
V |
5 | 2 | cv 1538 |
. . . . 5
class 𝑐 |
6 | 3 | cv 1538 |
. . . . . . 7
class ℎ |
7 | 6 | cdm 5589 |
. . . . . 6
class dom ℎ |
8 | 7 | cdm 5589 |
. . . . 5
class dom dom
ℎ |
9 | | cress 16941 |
. . . . 5
class
↾s |
10 | 5, 8, 9 | co 7275 |
. . . 4
class (𝑐 ↾s dom dom
ℎ) |
11 | | cnx 16894 |
. . . . . 6
class
ndx |
12 | | chom 16973 |
. . . . . 6
class
Hom |
13 | 11, 12 | cfv 6433 |
. . . . 5
class (Hom
‘ndx) |
14 | 13, 6 | cop 4567 |
. . . 4
class
〈(Hom ‘ndx), ℎ〉 |
15 | | csts 16864 |
. . . 4
class
sSet |
16 | 10, 14, 15 | co 7275 |
. . 3
class ((𝑐 ↾s dom dom
ℎ) sSet 〈(Hom
‘ndx), ℎ〉) |
17 | 2, 3, 4, 4, 16 | cmpo 7277 |
. 2
class (𝑐 ∈ V, ℎ ∈ V ↦ ((𝑐 ↾s dom dom ℎ) sSet 〈(Hom ‘ndx),
ℎ〉)) |
18 | 1, 17 | wceq 1539 |
1
wff
↾cat = (𝑐
∈ V, ℎ ∈ V ↦
((𝑐 ↾s dom
dom ℎ) sSet 〈(Hom
‘ndx), ℎ〉)) |