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

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

Detailed syntax breakdown of Definition df-2ndf
StepHypRef Expression
1 c2ndf 14272 . 2 F
2 vr . . 3
3 vs . . 3
4 ccat 13894 . . 3
5 vb . . . 4
62cv 1652 . . . . . 6
7 cbs 13474 . . . . . 6
86, 7cfv 5457 . . . . 5
93cv 1652 . . . . . 6
109, 7cfv 5457 . . . . 5
118, 10cxp 4879 . . . 4
12 c2nd 6351 . . . . . 6
135cv 1652 . . . . . 6
1412, 13cres 4883 . . . . 5
15 vx . . . . . 6
16 vy . . . . . 6
1715cv 1652 . . . . . . . 8
1816cv 1652 . . . . . . . 8
19 cxpc 14270 . . . . . . . . . 10 c
206, 9, 19co 6084 . . . . . . . . 9 c
21 chom 13545 . . . . . . . . 9
2220, 21cfv 5457 . . . . . . . 8 c
2317, 18, 22co 6084 . . . . . . 7 c
2412, 23cres 4883 . . . . . 6 c
2515, 16, 13, 13, 24cmpt2 6086 . . . . 5 c
2614, 25cop 3819 . . . 4 c
275, 11, 26csb 3253 . . 3 c
282, 3, 4, 4, 27cmpt2 6086 . 2 c
291, 28wceq 1653 1 F c
 Colors of variables: wff set class This definition is referenced by:  2ndfval  14296
 Copyright terms: Public domain W3C validator