Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-1stf Structured version   Unicode version

Definition df-1stf 15316
 Description: Define the first projection functor out of the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)
Assertion
Ref Expression
df-1stf F c
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-1stf
StepHypRef Expression
1 c1stf 15312 . 2 F
2 vr . . 3
3 vs . . 3
4 ccat 14938 . . 3
5 vb . . . 4
62cv 1382 . . . . . 6
7 cbs 14509 . . . . . 6
86, 7cfv 5578 . . . . 5
93cv 1382 . . . . . 6
109, 7cfv 5578 . . . . 5
118, 10cxp 4987 . . . 4
12 c1st 6783 . . . . . 6
135cv 1382 . . . . . 6
1412, 13cres 4991 . . . . 5
15 vx . . . . . 6
16 vy . . . . . 6
1715cv 1382 . . . . . . . 8
1816cv 1382 . . . . . . . 8
19 cxpc 15311 . . . . . . . . . 10 c
206, 9, 19co 6281 . . . . . . . . 9 c
21 chom 14585 . . . . . . . . 9
2220, 21cfv 5578 . . . . . . . 8 c
2317, 18, 22co 6281 . . . . . . 7 c
2412, 23cres 4991 . . . . . 6 c
2515, 16, 13, 13, 24cmpt2 6283 . . . . 5 c
2614, 25cop 4020 . . . 4 c
275, 11, 26csb 3420 . . 3 c
282, 3, 4, 4, 27cmpt2 6283 . 2 c
291, 28wceq 1383 1 F c
 Colors of variables: wff setvar class This definition is referenced by:  1stfval  15334
 Copyright terms: Public domain W3C validator