Definition df-1stf 18397

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 18393	. 2 class 1stF
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		ccat 17888	. . 3 class Cat
5		vb	. . . 4 setvar 𝑏
6	2	cv 1569	. . . . . 6 class 𝑟
7		cbs 17431	. . . . . 6 class Base
8	6, 7	cfv 6566	. . . . 5 class (Base‘𝑟)
9	3	cv 1569	. . . . . 6 class 𝑠
10	9, 7	cfv 6566	. . . . 5 class (Base‘𝑠)
11	8, 10	cxp 5656	. . . 4 class ((Base‘𝑟) × (Base‘𝑠))
12		c1st 8033	. . . . . 6 class 1st
13	5	cv 1569	. . . . . 6 class 𝑏
14	12, 13	cres 5660	. . . . 5 class (1st ↾ 𝑏)
15		vx	. . . . . 6 setvar 𝑥
16		vy	. . . . . 6 setvar 𝑦
17	15	cv 1569	. . . . . . . 8 class 𝑥
18	16	cv 1569	. . . . . . . 8 class 𝑦
19		cxpc 18392	. . . . . . . . . 10 class ×c
20	6, 9, 19	co 7451	. . . . . . . . 9 class (𝑟 ×c 𝑠)
21		chom 17483	. . . . . . . . 9 class Hom
22	20, 21	cfv 6566	. . . . . . . 8 class (Hom ‘(𝑟 ×c 𝑠))
23	17, 18, 22	co 7451	. . . . . . 7 class (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)
24	12, 23	cres 5660	. . . . . 6 class (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦))
25	15, 16, 13, 13, 24	cmpo 7453	. . . . 5 class (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))
26	14, 25	cop 4840	. . . 4 class ⟨(1st ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩
27	5, 11, 26	csb 3851	. . 3 class ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⟨(1st ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩
28	2, 3, 4, 4, 27	cmpo 7453	. 2 class (𝑟 ∈ Cat, 𝑠 ∈ Cat ↦ ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⟨(1st ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩)
29	1, 28	wceq 1570	1 wff 1stF = (𝑟 ∈ Cat, 𝑠 ∈ Cat ↦ ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⟨(1st ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩)

This definition is used by:  1stfval  18415  oppc1stf  50741