df-xpc - Metamath Proof Explorer

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

Definition df-xpc 16812

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**
Step	Hyp	Ref	Expression
1		cxpc 16808	. 2 _c
2		vr	. . 3
3		vs	. . 3
4		cvv 3200	. . 3
5		vb	. . . 4
6	2	cv 1482	. . . . . 6
7		cbs 15857	. . . . . 6
8	6, 7	cfv 5888	. . . . 5
9	3	cv 1482	. . . . . 6
10	9, 7	cfv 5888	. . . . 5
11	8, 10	cxp 5112	. . . 4
12		vh	. . . . 5
13		vu	. . . . . 6
14		vv	. . . . . 6
15	5	cv 1482	. . . . . 6
16	13	cv 1482	. . . . . . . . 9
17		c1st 7166	. . . . . . . . 9
18	16, 17	cfv 5888	. . . . . . . 8
19	14	cv 1482	. . . . . . . . 9
20	19, 17	cfv 5888	. . . . . . . 8
21		chom 15952	. . . . . . . . 9
22	6, 21	cfv 5888	. . . . . . . 8
23	18, 20, 22	co 6650	. . . . . . 7
24		c2nd 7167	. . . . . . . . 9
25	16, 24	cfv 5888	. . . . . . . 8
26	19, 24	cfv 5888	. . . . . . . 8
27	9, 21	cfv 5888	. . . . . . . 8
28	25, 26, 27	co 6650	. . . . . . 7
29	23, 28	cxp 5112	. . . . . 6
30	13, 14, 15, 15, 29	cmpt2 6652	. . . . 5
31		cnx 15854	. . . . . . . 8
32	31, 7	cfv 5888	. . . . . . 7
33	32, 15	cop 4183	. . . . . 6
34	31, 21	cfv 5888	. . . . . . 7
35	12	cv 1482	. . . . . . 7
36	34, 35	cop 4183	. . . . . 6
37		cco 15953	. . . . . . . 8 comp
38	31, 37	cfv 5888	. . . . . . 7 comp
39		vx	. . . . . . . 8
40		vy	. . . . . . . 8
41	15, 15	cxp 5112	. . . . . . . 8
42		vg	. . . . . . . . 9
43		vf	. . . . . . . . 9
44	39	cv 1482	. . . . . . . . . . 11
45	44, 24	cfv 5888	. . . . . . . . . 10
46	40	cv 1482	. . . . . . . . . 10
47	45, 46, 35	co 6650	. . . . . . . . 9
48	44, 35	cfv 5888	. . . . . . . . 9
49	42	cv 1482	. . . . . . . . . . . 12
50	49, 17	cfv 5888	. . . . . . . . . . 11
51	43	cv 1482	. . . . . . . . . . . 12
52	51, 17	cfv 5888	. . . . . . . . . . 11
53	44, 17	cfv 5888	. . . . . . . . . . . . . 14
54	53, 17	cfv 5888	. . . . . . . . . . . . 13
55	45, 17	cfv 5888	. . . . . . . . . . . . 13
56	54, 55	cop 4183	. . . . . . . . . . . 12
57	46, 17	cfv 5888	. . . . . . . . . . . 12
58	6, 37	cfv 5888	. . . . . . . . . . . 12 comp
59	56, 57, 58	co 6650	. . . . . . . . . . 11 comp
60	50, 52, 59	co 6650	. . . . . . . . . 10 comp
61	49, 24	cfv 5888	. . . . . . . . . . 11
62	51, 24	cfv 5888	. . . . . . . . . . 11
63	53, 24	cfv 5888	. . . . . . . . . . . . 13
64	45, 24	cfv 5888	. . . . . . . . . . . . 13
65	63, 64	cop 4183	. . . . . . . . . . . 12
66	46, 24	cfv 5888	. . . . . . . . . . . 12
67	9, 37	cfv 5888	. . . . . . . . . . . 12 comp
68	65, 66, 67	co 6650	. . . . . . . . . . 11 comp
69	61, 62, 68	co 6650	. . . . . . . . . 10 comp
70	60, 69	cop 4183	. . . . . . . . 9 comp comp
71	42, 43, 47, 48, 70	cmpt2 6652	. . . . . . . 8 comp comp
72	39, 40, 41, 15, 71	cmpt2 6652	. . . . . . 7 comp comp
73	38, 72	cop 4183	. . . . . 6 comp comp comp
74	33, 36, 73	ctp 4181	. . . . 5 comp comp comp
75	12, 30, 74	csb 3533	. . . 4 comp comp comp
76	5, 11, 75	csb 3533	. . 3 comp comp comp
77	2, 3, 4, 4, 76	cmpt2 6652	. 2 comp comp comp
78	1, 77	wceq 1483	1 _c comp comp comp

Colors of variables: wff setvar class

This definition is referenced by: fnxpc 16816 xpcval 16817

W3C validator