Definition df-1stf

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c1stf	⊢ 1stF
1		vr	⊢ 𝑟
2		ccat	⊢ Cat
3		vs	⊢ 𝑠
4		cbs	⊢ Base
5	1	cv	⊢ 𝑟
6	5 4	cfv	⊢ ( Base ‘ 𝑟 )
7	3	cv	⊢ 𝑠
8	7 4	cfv	⊢ ( Base ‘ 𝑠 )
9	6 8	cxp	⊢ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) )
10		vb	⊢ 𝑏
11		c1st	⊢ 1st
12	10	cv	⊢ 𝑏
13	11 12	cres	⊢ ( 1st ↾ 𝑏 )
14		vx	⊢ 𝑥
15		vy	⊢ 𝑦
16	14	cv	⊢ 𝑥
17		chom	⊢ Hom
18		cxpc	⊢ ×c
19	5 7 18	co	⊢ ( 𝑟 ×c 𝑠 )
20	19 17	cfv	⊢ ( Hom ‘ ( 𝑟 ×c 𝑠 ) )
21	15	cv	⊢ 𝑦
22	16 21 20	co	⊢ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 )
23	11 22	cres	⊢ ( 1st ↾ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) )
24	14 15 12 12 23	cmpo	⊢ ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) ) )
25	13 24	cop	⊢ ⟨ ( 1st ↾ 𝑏 ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) ) ) ⟩
26	10 9 25	csb	⊢ ⦋ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ⦌ ⟨ ( 1st ↾ 𝑏 ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) ) ) ⟩
27	1 3 2 2 26	cmpo	⊢ ( 𝑟 ∈ Cat , 𝑠 ∈ Cat ↦ ⦋ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ⦌ ⟨ ( 1st ↾ 𝑏 ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) ) ) ⟩ )
28	0 27	wceq	⊢ 1stF = ( 𝑟 ∈ Cat , 𝑠 ∈ Cat ↦ ⦋ ( ( Base ‘ 𝑟 ) × ( Base ‘ 𝑠 ) ) / 𝑏 ⦌ ⟨ ( 1st ↾ 𝑏 ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 1st ↾ ( 𝑥 ( Hom ‘ ( 𝑟 ×c 𝑠 ) ) 𝑦 ) ) ) ⟩ )