MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-resf Structured version   Visualization version   GIF version

Definition df-resf 17574
Description: Define the restriction of a functor to a subcategory (analogue of df-res 5603). (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
StepHypRef Expression
1 cresf 17570 . 2 class f
2 vf . . 3 setvar 𝑓
3 vh . . 3 setvar
4 cvv 3431 . . 3 class V
52cv 1538 . . . . . 6 class 𝑓
6 c1st 7829 . . . . . 6 class 1st
75, 6cfv 6435 . . . . 5 class (1st𝑓)
83cv 1538 . . . . . . 7 class
98cdm 5591 . . . . . 6 class dom
109cdm 5591 . . . . 5 class dom dom
117, 10cres 5593 . . . 4 class ((1st𝑓) ↾ dom dom )
12 vx . . . . 5 setvar 𝑥
1312cv 1538 . . . . . . 7 class 𝑥
14 c2nd 7830 . . . . . . . 8 class 2nd
155, 14cfv 6435 . . . . . . 7 class (2nd𝑓)
1613, 15cfv 6435 . . . . . 6 class ((2nd𝑓)‘𝑥)
1713, 8cfv 6435 . . . . . 6 class (𝑥)
1816, 17cres 5593 . . . . 5 class (((2nd𝑓)‘𝑥) ↾ (𝑥))
1912, 9, 18cmpt 5159 . . . 4 class (𝑥 ∈ dom ↦ (((2nd𝑓)‘𝑥) ↾ (𝑥)))
2011, 19cop 4569 . . 3 class ⟨((1st𝑓) ↾ dom dom ), (𝑥 ∈ dom ↦ (((2nd𝑓)‘𝑥) ↾ (𝑥)))⟩
212, 3, 4, 4, 20cmpo 7279 . 2 class (𝑓 ∈ V, ∈ V ↦ ⟨((1st𝑓) ↾ dom dom ), (𝑥 ∈ dom ↦ (((2nd𝑓)‘𝑥) ↾ (𝑥)))⟩)
221, 21wceq 1539 1 wff f = (𝑓 ∈ V, ∈ V ↦ ⟨((1st𝑓) ↾ dom dom ), (𝑥 ∈ dom ↦ (((2nd𝑓)‘𝑥) ↾ (𝑥)))⟩)
Colors of variables: wff setvar class
This definition is referenced by:  resfval  17605
  Copyright terms: Public domain W3C validator