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

Definition df-xpc 15298
 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 15294 . 2 c
2 vr . . 3
3 vs . . 3
4 cvv 3113 . . 3
5 vb . . . 4
62cv 1378 . . . . . 6
7 cbs 14489 . . . . . 6
86, 7cfv 5587 . . . . 5
93cv 1378 . . . . . 6
109, 7cfv 5587 . . . . 5
118, 10cxp 4997 . . . 4
12 vh . . . . 5
13 vu . . . . . 6
14 vv . . . . . 6
155cv 1378 . . . . . 6
1613cv 1378 . . . . . . . . 9
17 c1st 6782 . . . . . . . . 9
1816, 17cfv 5587 . . . . . . . 8
1914cv 1378 . . . . . . . . 9
2019, 17cfv 5587 . . . . . . . 8
21 chom 14565 . . . . . . . . 9
226, 21cfv 5587 . . . . . . . 8
2318, 20, 22co 6283 . . . . . . 7
24 c2nd 6783 . . . . . . . . 9
2516, 24cfv 5587 . . . . . . . 8
2619, 24cfv 5587 . . . . . . . 8
279, 21cfv 5587 . . . . . . . 8
2825, 26, 27co 6283 . . . . . . 7
2923, 28cxp 4997 . . . . . 6
3013, 14, 15, 15, 29cmpt2 6285 . . . . 5
31 cnx 14486 . . . . . . . 8
3231, 7cfv 5587 . . . . . . 7
3332, 15cop 4033 . . . . . 6
3431, 21cfv 5587 . . . . . . 7
3512cv 1378 . . . . . . 7
3634, 35cop 4033 . . . . . 6
37 cco 14566 . . . . . . . 8 comp
3831, 37cfv 5587 . . . . . . 7 comp
39 vx . . . . . . . 8
40 vy . . . . . . . 8
4115, 15cxp 4997 . . . . . . . 8
42 vg . . . . . . . . 9
43 vf . . . . . . . . 9
4439cv 1378 . . . . . . . . . . 11
4544, 24cfv 5587 . . . . . . . . . 10
4640cv 1378 . . . . . . . . . 10
4745, 46, 35co 6283 . . . . . . . . 9
4844, 35cfv 5587 . . . . . . . . 9
4942cv 1378 . . . . . . . . . . . 12
5049, 17cfv 5587 . . . . . . . . . . 11
5143cv 1378 . . . . . . . . . . . 12
5251, 17cfv 5587 . . . . . . . . . . 11
5344, 17cfv 5587 . . . . . . . . . . . . . 14
5453, 17cfv 5587 . . . . . . . . . . . . 13
5545, 17cfv 5587 . . . . . . . . . . . . 13
5654, 55cop 4033 . . . . . . . . . . . 12
5746, 17cfv 5587 . . . . . . . . . . . 12
586, 37cfv 5587 . . . . . . . . . . . 12 comp
5956, 57, 58co 6283 . . . . . . . . . . 11 comp
6050, 52, 59co 6283 . . . . . . . . . 10 comp
6149, 24cfv 5587 . . . . . . . . . . 11
6251, 24cfv 5587 . . . . . . . . . . 11
6353, 24cfv 5587 . . . . . . . . . . . . 13
6445, 24cfv 5587 . . . . . . . . . . . . 13
6563, 64cop 4033 . . . . . . . . . . . 12
6646, 24cfv 5587 . . . . . . . . . . . 12
679, 37cfv 5587 . . . . . . . . . . . 12 comp
6865, 66, 67co 6283 . . . . . . . . . . 11 comp
6961, 62, 68co 6283 . . . . . . . . . 10 comp
7060, 69cop 4033 . . . . . . . . 9 comp comp
7142, 43, 47, 48, 70cmpt2 6285 . . . . . . . 8 comp comp
7239, 40, 41, 15, 71cmpt2 6285 . . . . . . 7 comp comp
7338, 72cop 4033 . . . . . 6 comp comp comp
7433, 36, 73ctp 4031 . . . . 5 comp comp comp
7512, 30, 74csb 3435 . . . 4 comp comp comp
765, 11, 75csb 3435 . . 3 comp comp comp
772, 3, 4, 4, 76cmpt2 6285 . 2 comp comp comp
781, 77wceq 1379 1 c comp comp comp
 Colors of variables: wff setvar class This definition is referenced by:  fnxpc  15302  xpcval  15303
 Copyright terms: Public domain W3C validator