Detailed syntax breakdown of Definition df-resf
Step | Hyp | Ref
| Expression |
1 | | cresf 17570 |
. 2
class
↾f |
2 | | vf |
. . 3
setvar 𝑓 |
3 | | vh |
. . 3
setvar ℎ |
4 | | cvv 3431 |
. . 3
class
V |
5 | 2 | cv 1538 |
. . . . . 6
class 𝑓 |
6 | | c1st 7829 |
. . . . . 6
class
1st |
7 | 5, 6 | cfv 6435 |
. . . . 5
class
(1st ‘𝑓) |
8 | 3 | cv 1538 |
. . . . . . 7
class ℎ |
9 | 8 | cdm 5591 |
. . . . . 6
class dom ℎ |
10 | 9 | cdm 5591 |
. . . . 5
class dom dom
ℎ |
11 | 7, 10 | cres 5593 |
. . . 4
class
((1st ‘𝑓) ↾ dom dom ℎ) |
12 | | vx |
. . . . 5
setvar 𝑥 |
13 | 12 | cv 1538 |
. . . . . . 7
class 𝑥 |
14 | | c2nd 7830 |
. . . . . . . 8
class
2nd |
15 | 5, 14 | cfv 6435 |
. . . . . . 7
class
(2nd ‘𝑓) |
16 | 13, 15 | cfv 6435 |
. . . . . 6
class
((2nd ‘𝑓)‘𝑥) |
17 | 13, 8 | cfv 6435 |
. . . . . 6
class (ℎ‘𝑥) |
18 | 16, 17 | cres 5593 |
. . . . 5
class
(((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)) |
19 | 12, 9, 18 | cmpt 5159 |
. . . 4
class (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥))) |
20 | 11, 19 | cop 4569 |
. . 3
class
〈((1st ‘𝑓) ↾ dom dom ℎ), (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))〉 |
21 | 2, 3, 4, 4, 20 | cmpo 7279 |
. 2
class (𝑓 ∈ V, ℎ ∈ V ↦ 〈((1st
‘𝑓) ↾ dom dom
ℎ), (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))〉) |
22 | 1, 21 | wceq 1539 |
1
wff
↾f = (𝑓 ∈ V, ℎ ∈ V ↦ 〈((1st
‘𝑓) ↾ dom dom
ℎ), (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))〉) |