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

Definition df-2ndf 17036
Description: Define the second projection functor out of the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
Assertion
Ref Expression
df-2ndf 2ndF = (𝑟 ∈ Cat, 𝑠 ∈ Cat ↦ ((Base‘𝑟) × (Base‘𝑠)) / 𝑏⟨(2nd𝑏), (𝑥𝑏, 𝑦𝑏 ↦ (2nd ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩)
Distinct variable group:   𝑟,𝑏,𝑠,𝑥,𝑦

Detailed syntax breakdown of Definition df-2ndf
StepHypRef Expression
1 c2ndf 17032 . 2 class 2ndF
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 ccat 16547 . . 3 class Cat
5 vb . . . 4 setvar 𝑏
62cv 1631 . . . . . 6 class 𝑟
7 cbs 16080 . . . . . 6 class Base
86, 7cfv 6050 . . . . 5 class (Base‘𝑟)
93cv 1631 . . . . . 6 class 𝑠
109, 7cfv 6050 . . . . 5 class (Base‘𝑠)
118, 10cxp 5265 . . . 4 class ((Base‘𝑟) × (Base‘𝑠))
12 c2nd 7334 . . . . . 6 class 2nd
135cv 1631 . . . . . 6 class 𝑏
1412, 13cres 5269 . . . . 5 class (2nd𝑏)
15 vx . . . . . 6 setvar 𝑥
16 vy . . . . . 6 setvar 𝑦
1715cv 1631 . . . . . . . 8 class 𝑥
1816cv 1631 . . . . . . . 8 class 𝑦
19 cxpc 17030 . . . . . . . . . 10 class ×c
206, 9, 19co 6815 . . . . . . . . 9 class (𝑟 ×c 𝑠)
21 chom 16175 . . . . . . . . 9 class Hom
2220, 21cfv 6050 . . . . . . . 8 class (Hom ‘(𝑟 ×c 𝑠))
2317, 18, 22co 6815 . . . . . . 7 class (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)
2412, 23cres 5269 . . . . . 6 class (2nd ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦))
2515, 16, 13, 13, 24cmpt2 6817 . . . . 5 class (𝑥𝑏, 𝑦𝑏 ↦ (2nd ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))
2614, 25cop 4328 . . . 4 class ⟨(2nd𝑏), (𝑥𝑏, 𝑦𝑏 ↦ (2nd ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩
275, 11, 26csb 3675 . . 3 class ((Base‘𝑟) × (Base‘𝑠)) / 𝑏⟨(2nd𝑏), (𝑥𝑏, 𝑦𝑏 ↦ (2nd ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩
282, 3, 4, 4, 27cmpt2 6817 . 2 class (𝑟 ∈ Cat, 𝑠 ∈ Cat ↦ ((Base‘𝑟) × (Base‘𝑠)) / 𝑏⟨(2nd𝑏), (𝑥𝑏, 𝑦𝑏 ↦ (2nd ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩)
291, 28wceq 1632 1 wff 2ndF = (𝑟 ∈ Cat, 𝑠 ∈ Cat ↦ ((Base‘𝑟) × (Base‘𝑠)) / 𝑏⟨(2nd𝑏), (𝑥𝑏, 𝑦𝑏 ↦ (2nd ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩)
Colors of variables: wff setvar class
This definition is referenced by:  2ndfval  17056
  Copyright terms: Public domain W3C validator