Definition df-resf 18029

Description: Define the restriction of a functor to a subcategory (analogue of df-res 5663). (Contributed by Mario Carneiro, 6-Jan-2017.)

Assertion

Ref	Expression
df-resf	⊢ ↾f = (𝑓 ∈ V, ℎ ∈ V ↦ ⟨((1st ‘𝑓) ↾ dom dom ℎ), (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))⟩)

Distinct variable group:   𝑓,ℎ,𝑥

Detailed syntax breakdown of Definition df-resf

Step	Hyp	Ref	Expression
1		cresf 18025	. 2 class ↾f
2		vf	. . 3 setvar 𝑓
3		vh	. . 3 setvar ℎ
4		cvv 3451	. . 3 class V
5	2	cv 1569	. . . . . 6 class 𝑓
6		c1st 7997	. . . . . 6 class 1st
7	5, 6	cfv 6537	. . . . 5 class (1st ‘𝑓)
8	3	cv 1569	. . . . . . 7 class ℎ
9	8	cdm 5651	. . . . . 6 class dom ℎ
10	9	cdm 5651	. . . . 5 class dom dom ℎ
11	7, 10	cres 5653	. . . 4 class ((1st ‘𝑓) ↾ dom dom ℎ)
12		vx	. . . . 5 setvar 𝑥
13	12	cv 1569	. . . . . . 7 class 𝑥
14		c2nd 7998	. . . . . . . 8 class 2nd
15	5, 14	cfv 6537	. . . . . . 7 class (2nd ‘𝑓)
16	13, 15	cfv 6537	. . . . . 6 class ((2nd ‘𝑓)‘𝑥)
17	13, 8	cfv 6537	. . . . . 6 class (ℎ‘𝑥)
18	16, 17	cres 5653	. . . . 5 class (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥))
19	12, 9, 18	cmpt 5186	. . . 4 class (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))
20	11, 19	cop 4590	. . 3 class ⟨((1st ‘𝑓) ↾ dom dom ℎ), (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))⟩
21	2, 3, 4, 4, 20	cmpo 7420	. 2 class (𝑓 ∈ V, ℎ ∈ V ↦ ⟨((1st ‘𝑓) ↾ dom dom ℎ), (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))⟩)
22	1, 21	wceq 1570	1 wff ↾f = (𝑓 ∈ V, ℎ ∈ V ↦ ⟨((1st ‘𝑓) ↾ dom dom ℎ), (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))⟩)

This definition is used by:  resfval  18060