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} = (f \in V, h \in V ⟼ ⟨{1^{st} (f) ↾}_{dom dom h}, (x \in dom h ⟼ {2^{nd} (f) (x) ↾}_{h (x)})⟩)$

Step	Hyp	Ref	Expression
0		cresf	$class ↾_{f}$
1		vf	$setvar f$
2		cvv	$class V$
3		vh	$setvar h$
4		c1st	$class 1^{st}$
5	1	cv	$setvar f$
6	5 4	cfv	$class 1^{st} (f)$
7	3	cv	$setvar h$
8	7	cdm	$class dom h$
9	8	cdm	$class dom dom h$
10	6 9	cres	$class ({1^{st} (f) ↾}_{dom dom h})$
11		vx	$setvar x$
12		c2nd	$class 2^{nd}$
13	5 12	cfv	$class 2^{nd} (f)$
14	11	cv	$setvar x$
15	14 13	cfv	$class 2^{nd} (f) (x)$
16	14 7	cfv	$class h (x)$
17	15 16	cres	$class ({2^{nd} (f) (x) ↾}_{h (x)})$
18	11 8 17	cmpt	$class (x \in dom h ⟼ {2^{nd} (f) (x) ↾}_{h (x)})$
19	10 18	cop	$class ⟨{1^{st} (f) ↾}_{dom dom h}, (x \in dom h ⟼ {2^{nd} (f) (x) ↾}_{h (x)})⟩$
20	1 3 2 2 19	cmpo	$class (f \in V, h \in V ⟼ ⟨{1^{st} (f) ↾}_{dom dom h}, (x \in dom h ⟼ {2^{nd} (f) (x) ↾}_{h (x)})⟩)$
21	0 20	wceq	$wff ↾_{f} = (f \in V, h \in V ⟼ ⟨{1^{st} (f) ↾}_{dom dom h}, (x \in dom h ⟼ {2^{nd} (f) (x) ↾}_{h (x)})⟩)$

Metamath Proof Explorer