Definition df-2ndf 18328

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

Step	Hyp	Ref	Expression
1		c2ndf 18324	. 2 class 2ndF
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		ccat 17818	. . 3 class Cat
5		vb	. . . 4 setvar 𝑏
6	2	cv 1569	. . . . . 6 class 𝑟
7		cbs 17367	. . . . . 6 class Base
8	6, 7	cfv 6531	. . . . 5 class (Base‘𝑟)
9	3	cv 1569	. . . . . 6 class 𝑠
10	9, 7	cfv 6531	. . . . 5 class (Base‘𝑠)
11	8, 10	cxp 5649	. . . 4 class ((Base‘𝑟) × (Base‘𝑠))
12		c2nd 7989	. . . . . 6 class 2nd
13	5	cv 1569	. . . . . 6 class 𝑏
14	12, 13	cres 5653	. . . . 5 class (2nd ↾ 𝑏)
15		vx	. . . . . 6 setvar 𝑥
16		vy	. . . . . 6 setvar 𝑦
17	15	cv 1569	. . . . . . . 8 class 𝑥
18	16	cv 1569	. . . . . . . 8 class 𝑦
19		cxpc 18322	. . . . . . . . . 10 class ×c
20	6, 9, 19	co 7412	. . . . . . . . 9 class (𝑟 ×c 𝑠)
21		chom 17419	. . . . . . . . 9 class Hom
22	20, 21	cfv 6531	. . . . . . . 8 class (Hom ‘(𝑟 ×c 𝑠))
23	17, 18, 22	co 7412	. . . . . . 7 class (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)
24	12, 23	cres 5653	. . . . . 6 class (2nd ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦))
25	15, 16, 13, 13, 24	cmpo 7414	. . . . 5 class (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (2nd ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))
26	14, 25	cop 4590	. . . 4 class ⟨(2nd ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (2nd ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩
27	5, 11, 26	csb 3847	. . 3 class ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⟨(2nd ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (2nd ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩
28	2, 3, 4, 4, 27	cmpo 7414	. 2 class (𝑟 ∈ Cat, 𝑠 ∈ Cat ↦ ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⟨(2nd ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (2nd ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩)
29	1, 28	wceq 1570	1 wff 2ndF = (𝑟 ∈ Cat, 𝑠 ∈ Cat ↦ ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⟨(2nd ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (2nd ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩)

This definition is used by:  2ndfval  18348  oppc2ndf  50341