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

Definition df-2ndf 15765
 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 15761 . 2 F
2 vr . . 3
3 vs . . 3
4 ccat 15276 . . 3
5 vb . . . 4
62cv 1404 . . . . . 6
7 cbs 14839 . . . . . 6
86, 7cfv 5568 . . . . 5
93cv 1404 . . . . . 6
109, 7cfv 5568 . . . . 5
118, 10cxp 4820 . . . 4
12 c2nd 6782 . . . . . 6
135cv 1404 . . . . . 6
1412, 13cres 4824 . . . . 5
15 vx . . . . . 6
16 vy . . . . . 6
1715cv 1404 . . . . . . . 8
1816cv 1404 . . . . . . . 8
19 cxpc 15759 . . . . . . . . . 10 c
206, 9, 19co 6277 . . . . . . . . 9 c
21 chom 14918 . . . . . . . . 9
2220, 21cfv 5568 . . . . . . . 8 c
2317, 18, 22co 6277 . . . . . . 7 c
2412, 23cres 4824 . . . . . 6 c
2515, 16, 13, 13, 24cmpt2 6279 . . . . 5 c
2614, 25cop 3977 . . . 4 c
275, 11, 26csb 3372 . . 3 c
282, 3, 4, 4, 27cmpt2 6279 . 2 c
291, 28wceq 1405 1 F c
 Colors of variables: wff setvar class This definition is referenced by:  2ndfval  15785
 Copyright terms: Public domain W3C validator