Definition df-1stf 17806

Description: Define the first projection functor out of the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)

Assertion

Ref	Expression
df-1stf	⊢ 1stF = (𝑟 ∈ Cat, 𝑠 ∈ Cat ↦ ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⟨(1st ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩)

Distinct variable group:   𝑟,𝑏,𝑠,𝑥,𝑦

Detailed syntax breakdown of Definition df-1stf

Step	Hyp	Ref	Expression
1		c1stf 17802	. 2 class 1stF
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		ccat 17290	. . 3 class Cat
5		vb	. . . 4 setvar 𝑏
6	2	cv 1538	. . . . . 6 class 𝑟
7		cbs 16840	. . . . . 6 class Base
8	6, 7	cfv 6418	. . . . 5 class (Base‘𝑟)
9	3	cv 1538	. . . . . 6 class 𝑠
10	9, 7	cfv 6418	. . . . 5 class (Base‘𝑠)
11	8, 10	cxp 5578	. . . 4 class ((Base‘𝑟) × (Base‘𝑠))
12		c1st 7802	. . . . . 6 class 1st
13	5	cv 1538	. . . . . 6 class 𝑏
14	12, 13	cres 5582	. . . . 5 class (1st ↾ 𝑏)
15		vx	. . . . . 6 setvar 𝑥
16		vy	. . . . . 6 setvar 𝑦
17	15	cv 1538	. . . . . . . 8 class 𝑥
18	16	cv 1538	. . . . . . . 8 class 𝑦
19		cxpc 17801	. . . . . . . . . 10 class ×c
20	6, 9, 19	co 7255	. . . . . . . . 9 class (𝑟 ×c 𝑠)
21		chom 16899	. . . . . . . . 9 class Hom
22	20, 21	cfv 6418	. . . . . . . 8 class (Hom ‘(𝑟 ×c 𝑠))
23	17, 18, 22	co 7255	. . . . . . 7 class (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)
24	12, 23	cres 5582	. . . . . 6 class (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦))
25	15, 16, 13, 13, 24	cmpo 7257	. . . . 5 class (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))
26	14, 25	cop 4564	. . . 4 class ⟨(1st ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩
27	5, 11, 26	csb 3828	. . 3 class ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⟨(1st ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩
28	2, 3, 4, 4, 27	cmpo 7257	. 2 class (𝑟 ∈ Cat, 𝑠 ∈ Cat ↦ ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⟨(1st ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩)
29	1, 28	wceq 1539	1 wff 1stF = (𝑟 ∈ Cat, 𝑠 ∈ Cat ↦ ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⟨(1st ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩)

This definition is referenced by:  1stfval  17824