Definition df-resf 17557

Description: Define the restriction of a functor to a subcategory (analogue of df-res 5600). (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 17553	. 2 class ↾f
2		vf	. . 3 setvar 𝑓
3		vh	. . 3 setvar ℎ
4		cvv 3430	. . 3 class V
5	2	cv 1540	. . . . . 6 class 𝑓
6		c1st 7815	. . . . . 6 class 1st
7	5, 6	cfv 6430	. . . . 5 class (1st ‘𝑓)
8	3	cv 1540	. . . . . . 7 class ℎ
9	8	cdm 5588	. . . . . 6 class dom ℎ
10	9	cdm 5588	. . . . 5 class dom dom ℎ
11	7, 10	cres 5590	. . . 4 class ((1st ‘𝑓) ↾ dom dom ℎ)
12		vx	. . . . 5 setvar 𝑥
13	12	cv 1540	. . . . . . 7 class 𝑥
14		c2nd 7816	. . . . . . . 8 class 2nd
15	5, 14	cfv 6430	. . . . . . 7 class (2nd ‘𝑓)
16	13, 15	cfv 6430	. . . . . 6 class ((2nd ‘𝑓)‘𝑥)
17	13, 8	cfv 6430	. . . . . 6 class (ℎ‘𝑥)
18	16, 17	cres 5590	. . . . 5 class (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥))
19	12, 9, 18	cmpt 5161	. . . 4 class (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))
20	11, 19	cop 4572	. . 3 class ⟨((1st ‘𝑓) ↾ dom dom ℎ), (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))⟩
21	2, 3, 4, 4, 20	cmpo 7270	. 2 class (𝑓 ∈ V, ℎ ∈ V ↦ ⟨((1st ‘𝑓) ↾ dom dom ℎ), (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))⟩)
22	1, 21	wceq 1541	1 wff ↾f = (𝑓 ∈ V, ℎ ∈ V ↦ ⟨((1st ‘𝑓) ↾ dom dom ℎ), (𝑥 ∈ dom ℎ ↦ (((2nd ‘𝑓)‘𝑥) ↾ (ℎ‘𝑥)))⟩)

This definition is referenced by:  resfval  17588