Metamath Proof Explorer


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 1 st F = r Cat , s Cat Base r × Base s / b 1 st b x b , y b 1 st x Hom r × c s y

Detailed syntax breakdown

Step Hyp Ref Expression
0 c1stf class 1 st F
1 vr setvar r
2 ccat class Cat
3 vs setvar s
4 cbs class Base
5 1 cv setvar r
6 5 4 cfv class Base r
7 3 cv setvar s
8 7 4 cfv class Base s
9 6 8 cxp class Base r × Base s
10 vb setvar b
11 c1st class 1 st
12 10 cv setvar b
13 11 12 cres class 1 st b
14 vx setvar x
15 vy setvar y
16 14 cv setvar x
17 chom class Hom
18 cxpc class × c
19 5 7 18 co class r × c s
20 19 17 cfv class Hom r × c s
21 15 cv setvar y
22 16 21 20 co class x Hom r × c s y
23 11 22 cres class 1 st x Hom r × c s y
24 14 15 12 12 23 cmpo class x b , y b 1 st x Hom r × c s y
25 13 24 cop class 1 st b x b , y b 1 st x Hom r × c s y
26 10 9 25 csb class Base r × Base s / b 1 st b x b , y b 1 st x Hom r × c s y
27 1 3 2 2 26 cmpo class r Cat , s Cat Base r × Base s / b 1 st b x b , y b 1 st x Hom r × c s y
28 0 27 wceq wff 1 st F = r Cat , s Cat Base r × Base s / b 1 st b x b , y b 1 st x Hom r × c s y