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

Definition df-xpc 14271
 Description: Define the binary product of categories, which has objects for each pair of objects of the factors, and morphisms for each pair of morphisms of the factors. Composition is componentwise. (Contributed by Mario Carneiro, 10-Jan-2017.)
Assertion
Ref Expression
df-xpc c comp comp comp
Distinct variable group:   ,,,,,,,,,

Detailed syntax breakdown of Definition df-xpc
StepHypRef Expression
1 cxpc 14267 . 2 c
2 vr . . 3
3 vs . . 3
4 cvv 2958 . . 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 vh . . . . 5
13 vu . . . . . 6
14 vv . . . . . 6
155cv 1652 . . . . . 6
1613cv 1652 . . . . . . . . 9
17 c1st 6349 . . . . . . . . 9
1816, 17cfv 5456 . . . . . . . 8
1914cv 1652 . . . . . . . . 9
2019, 17cfv 5456 . . . . . . . 8
21 chom 13542 . . . . . . . . 9
226, 21cfv 5456 . . . . . . . 8
2318, 20, 22co 6083 . . . . . . 7
24 c2nd 6350 . . . . . . . . 9
2516, 24cfv 5456 . . . . . . . 8
2619, 24cfv 5456 . . . . . . . 8
279, 21cfv 5456 . . . . . . . 8
2825, 26, 27co 6083 . . . . . . 7
2923, 28cxp 4878 . . . . . 6
3013, 14, 15, 15, 29cmpt2 6085 . . . . 5
31 cnx 13468 . . . . . . . 8
3231, 7cfv 5456 . . . . . . 7
3332, 15cop 3819 . . . . . 6
3431, 21cfv 5456 . . . . . . 7
3512cv 1652 . . . . . . 7
3634, 35cop 3819 . . . . . 6
37 cco 13543 . . . . . . . 8 comp
3831, 37cfv 5456 . . . . . . 7 comp
39 vx . . . . . . . 8
40 vy . . . . . . . 8
4115, 15cxp 4878 . . . . . . . 8
42 vg . . . . . . . . 9
43 vf . . . . . . . . 9
4439cv 1652 . . . . . . . . . . 11
4544, 24cfv 5456 . . . . . . . . . 10
4640cv 1652 . . . . . . . . . 10
4745, 46, 35co 6083 . . . . . . . . 9
4844, 35cfv 5456 . . . . . . . . 9
4942cv 1652 . . . . . . . . . . . 12
5049, 17cfv 5456 . . . . . . . . . . 11
5143cv 1652 . . . . . . . . . . . 12
5251, 17cfv 5456 . . . . . . . . . . 11
5344, 17cfv 5456 . . . . . . . . . . . . . 14
5453, 17cfv 5456 . . . . . . . . . . . . 13
5545, 17cfv 5456 . . . . . . . . . . . . 13
5654, 55cop 3819 . . . . . . . . . . . 12
5746, 17cfv 5456 . . . . . . . . . . . 12
586, 37cfv 5456 . . . . . . . . . . . 12 comp
5956, 57, 58co 6083 . . . . . . . . . . 11 comp
6050, 52, 59co 6083 . . . . . . . . . 10 comp
6149, 24cfv 5456 . . . . . . . . . . 11
6251, 24cfv 5456 . . . . . . . . . . 11
6353, 24cfv 5456 . . . . . . . . . . . . 13
6445, 24cfv 5456 . . . . . . . . . . . . 13
6563, 64cop 3819 . . . . . . . . . . . 12
6646, 24cfv 5456 . . . . . . . . . . . 12
679, 37cfv 5456 . . . . . . . . . . . 12 comp
6865, 66, 67co 6083 . . . . . . . . . . 11 comp
6961, 62, 68co 6083 . . . . . . . . . 10 comp
7060, 69cop 3819 . . . . . . . . 9 comp comp
7142, 43, 47, 48, 70cmpt2 6085 . . . . . . . 8 comp comp
7239, 40, 41, 15, 71cmpt2 6085 . . . . . . 7 comp comp
7338, 72cop 3819 . . . . . 6 comp comp comp
7433, 36, 73ctp 3818 . . . . 5 comp comp comp
7512, 30, 74csb 3253 . . . 4 comp comp comp
765, 11, 75csb 3253 . . 3 comp comp comp
772, 3, 4, 4, 76cmpt2 6085 . 2 comp comp comp
781, 77wceq 1653 1 c comp comp comp
 Colors of variables: wff set class This definition is referenced by:  fnxpc  14275  xpcval  14276
 Copyright terms: Public domain W3C validator