df-resf

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

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

Step	Hyp	Ref	Expression
0		cresf	⊢ ↾_f
1		vf	⊢ 𝑓
2		cvv	⊢ V
3		vh	⊢ ℎ
4		c1st	⊢ 1^st
5	1	cv	⊢ 𝑓
6	5 4	cfv	⊢ ( 1^st ‘ 𝑓 )
7	3	cv	⊢ ℎ
8	7	cdm	⊢ dom ℎ
9	8	cdm	⊢ dom dom ℎ
10	6 9	cres	⊢ ( ( 1^st ‘ 𝑓 ) ↾ dom dom ℎ )
11		vx	⊢ 𝑥
12		c2nd	⊢ 2^nd
13	5 12	cfv	⊢ ( 2^nd ‘ 𝑓 )
14	11	cv	⊢ 𝑥
15	14 13	cfv	⊢ ( ( 2^nd ‘ 𝑓 ) ‘ 𝑥 )
16	14 7	cfv	⊢ ( ℎ ‘ 𝑥 )
17	15 16	cres	⊢ ( ( ( 2^nd ‘ 𝑓 ) ‘ 𝑥 ) ↾ ( ℎ ‘ 𝑥 ) )
18	11 8 17	cmpt	⊢ ( 𝑥 ∈ dom ℎ ↦ ( ( ( 2^nd ‘ 𝑓 ) ‘ 𝑥 ) ↾ ( ℎ ‘ 𝑥 ) ) )
19	10 18	cop	⊢ ⟨ ( ( 1^st ‘ 𝑓 ) ↾ dom dom ℎ ) , ( 𝑥 ∈ dom ℎ ↦ ( ( ( 2^nd ‘ 𝑓 ) ‘ 𝑥 ) ↾ ( ℎ ‘ 𝑥 ) ) ) ⟩
20	1 3 2 2 19	cmpo	⊢ ( 𝑓 ∈ V , ℎ ∈ V ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ↾ dom dom ℎ ) , ( 𝑥 ∈ dom ℎ ↦ ( ( ( 2^nd ‘ 𝑓 ) ‘ 𝑥 ) ↾ ( ℎ ‘ 𝑥 ) ) ) ⟩ )
21	0 20	wceq	⊢ ↾_f = ( 𝑓 ∈ V , ℎ ∈ V ↦ ⟨ ( ( 1^st ‘ 𝑓 ) ↾ dom dom ℎ ) , ( 𝑥 ∈ dom ℎ ↦ ( ( ( 2^nd ‘ 𝑓 ) ‘ 𝑥 ) ↾ ( ℎ ‘ 𝑥 ) ) ) ⟩ )

Metamath Proof Explorer