Definition df-1stf 18098

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 18094	. 2 class 1stF
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		ccat 17589	. . 3 class Cat
5		vb	. . . 4 setvar 𝑏
6	2	cv 1539	. . . . . 6 class 𝑟
7		cbs 17139	. . . . . 6 class Base
8	6, 7	cfv 6486	. . . . 5 class (Base‘𝑟)
9	3	cv 1539	. . . . . 6 class 𝑠
10	9, 7	cfv 6486	. . . . 5 class (Base‘𝑠)
11	8, 10	cxp 5621	. . . 4 class ((Base‘𝑟) × (Base‘𝑠))
12		c1st 7929	. . . . . 6 class 1st
13	5	cv 1539	. . . . . 6 class 𝑏
14	12, 13	cres 5625	. . . . 5 class (1st ↾ 𝑏)
15		vx	. . . . . 6 setvar 𝑥
16		vy	. . . . . 6 setvar 𝑦
17	15	cv 1539	. . . . . . . 8 class 𝑥
18	16	cv 1539	. . . . . . . 8 class 𝑦
19		cxpc 18093	. . . . . . . . . 10 class ×c
20	6, 9, 19	co 7353	. . . . . . . . 9 class (𝑟 ×c 𝑠)
21		chom 17191	. . . . . . . . 9 class Hom
22	20, 21	cfv 6486	. . . . . . . 8 class (Hom ‘(𝑟 ×c 𝑠))
23	17, 18, 22	co 7353	. . . . . . 7 class (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)
24	12, 23	cres 5625	. . . . . 6 class (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦))
25	15, 16, 13, 13, 24	cmpo 7355	. . . . 5 class (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))
26	14, 25	cop 4585	. . . 4 class ⟨(1st ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩
27	5, 11, 26	csb 3853	. . 3 class ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⟨(1st ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩
28	2, 3, 4, 4, 27	cmpo 7355	. 2 class (𝑟 ∈ Cat, 𝑠 ∈ Cat ↦ ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⟨(1st ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩)
29	1, 28	wceq 1540	1 wff 1stF = (𝑟 ∈ Cat, 𝑠 ∈ Cat ↦ ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⟨(1st ↾ 𝑏), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (1st ↾ (𝑥(Hom ‘(𝑟 ×c 𝑠))𝑦)))⟩)

This definition is referenced by:  1stfval  18116  oppc1stf  49293