Metamath Proof Explorer

Definition 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 ∈ V , h ∈ V ⟼ 1 st ⁡ f ↾ dom ⁡ dom ⁡ h x ∈ dom ⁡ h ⟼ 2 nd ⁡ f ⁡ x ↾ h ⁡ x

Detailed syntax breakdown

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 ∈ dom ⁡ h ⟼ 2 nd ⁡ f ⁡ x ↾ h ⁡ x
19 10 18 cop class 1 st ⁡ f ↾ dom ⁡ dom ⁡ h x ∈ dom ⁡ h ⟼ 2 nd ⁡ f ⁡ x ↾ h ⁡ x
20 1 3 2 2 19 cmpo class f ∈ V , h ∈ V ⟼ 1 st ⁡ f ↾ dom ⁡ dom ⁡ h x ∈ dom ⁡ h ⟼ 2 nd ⁡ f ⁡ x ↾ h ⁡ x
21 0 20 wceq wff ↾ f = f ∈ V , h ∈ V ⟼ 1 st ⁡ f ↾ dom ⁡ dom ⁡ h x ∈ dom ⁡ h ⟼ 2 nd ⁡ f ⁡ x ↾ h ⁡ x