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

Definition df-1stf 14272
 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 14268 . 2 F
2 vr . . 3
3 vs . . 3
4 ccat 13891 . . 3
5 vb . . . 4
62cv 1652 . . . . . 6
7 cbs 13471 . . . . . 6
86, 7cfv 5456 . . . . 5
93cv 1652 . . . . . 6
109, 7cfv 5456 . . . . 5
118, 10cxp 4878 . . . 4
12 c1st 6349 . . . . . 6
135cv 1652 . . . . . 6
1412, 13cres 4882 . . . . 5
15 vx . . . . . 6
16 vy . . . . . 6
1715cv 1652 . . . . . . . 8
1816cv 1652 . . . . . . . 8
19 cxpc 14267 . . . . . . . . . 10 c
206, 9, 19co 6083 . . . . . . . . 9 c
21 chom 13542 . . . . . . . . 9
2220, 21cfv 5456 . . . . . . . 8 c
2317, 18, 22co 6083 . . . . . . 7 c
2412, 23cres 4882 . . . . . 6 c
2515, 16, 13, 13, 24cmpt2 6085 . . . . 5 c
2614, 25cop 3819 . . . 4 c
275, 11, 26csb 3253 . . 3 c
282, 3, 4, 4, 27cmpt2 6085 . 2 c
291, 28wceq 1653 1 F c
 Colors of variables: wff set class This definition is referenced by:  1stfval  14290
 Copyright terms: Public domain W3C validator