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 16293
Description: Define the restriction of a functor to a subcategory (analogue of df-res 5040). (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 16289 . 2 class f
2 vf . . 3 setvar 𝑓
3 vh . . 3 setvar
4 cvv 3173 . . 3 class V
52cv 1474 . . . . . 6 class 𝑓
6 c1st 7035 . . . . . 6 class 1st
75, 6cfv 5790 . . . . 5 class (1st𝑓)
83cv 1474 . . . . . . 7 class
98cdm 5028 . . . . . 6 class dom
109cdm 5028 . . . . 5 class dom dom
117, 10cres 5030 . . . 4 class ((1st𝑓) ↾ dom dom )
12 vx . . . . 5 setvar 𝑥
1312cv 1474 . . . . . . 7 class 𝑥
14 c2nd 7036 . . . . . . . 8 class 2nd
155, 14cfv 5790 . . . . . . 7 class (2nd𝑓)
1613, 15cfv 5790 . . . . . 6 class ((2nd𝑓)‘𝑥)
1713, 8cfv 5790 . . . . . 6 class (𝑥)
1816, 17cres 5030 . . . . 5 class (((2nd𝑓)‘𝑥) ↾ (𝑥))
1912, 9, 18cmpt 4638 . . . 4 class (𝑥 ∈ dom ↦ (((2nd𝑓)‘𝑥) ↾ (𝑥)))
2011, 19cop 4131 . . 3 class ⟨((1st𝑓) ↾ dom dom ), (𝑥 ∈ dom ↦ (((2nd𝑓)‘𝑥) ↾ (𝑥)))⟩
212, 3, 4, 4, 20cmpt2 6529 . 2 class (𝑓 ∈ V, ∈ V ↦ ⟨((1st𝑓) ↾ dom dom ), (𝑥 ∈ dom ↦ (((2nd𝑓)‘𝑥) ↾ (𝑥)))⟩)
221, 21wceq 1475 1 wff f = (𝑓 ∈ V, ∈ V ↦ ⟨((1st𝑓) ↾ dom dom ), (𝑥 ∈ dom ↦ (((2nd𝑓)‘𝑥) ↾ (𝑥)))⟩)
Colors of variables: wff setvar class
This definition is referenced by:  resfval  16324
  Copyright terms: Public domain W3C validator