Definition df-xpc

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)

	Ref	Expression
Assertion	df-xpc	$$⊢{\times }_c=\left(r\in \mathrm{V},s\in \mathrm{V}⟼⦋\left({\mathrm{Base}}_r\times {\mathrm{Base}}_s\right)/b⦌⦋\left(u\in b,v\in b⟼\left(1^{st}\left(u\right)\mathrm{Hom}\left(r\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(s\right)2^{nd}\left(v\right)\right)\right)/h⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),h⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(x\in \left(b\times b\right),y\in b⟼\left(g\in \left(2^{nd}\left(x\right)hy\right),f\in h\left(x\right)⟼⟨1^{st}\left(g\right)\left(⟨1^{st}\left(1^{st}\left(x\right)\right),1^{st}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(r\right)1^{st}\left(y\right)\right)1^{st}\left(f\right),2^{nd}\left(g\right)\left(⟨2^{nd}\left(1^{st}\left(x\right)\right),2^{nd}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(s\right)2^{nd}\left(y\right)\right)2^{nd}\left(f\right)⟩\right)\right)⟩\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cxpc	$$class{\times }_c$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		vs	$$setvars$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarr$$
6	5 4	cfv	$$class{\mathrm{Base}}_r$$
7	3	cv	$$setvars$$
8	7 4	cfv	$$class{\mathrm{Base}}_s$$
9	6 8	cxp	$$class\left({\mathrm{Base}}_r\times {\mathrm{Base}}_s\right)$$
10		vb	$$setvarb$$
11		vu	$$setvaru$$
12	10	cv	$$setvarb$$
13		vv	$$setvarv$$
14		c1st	$$class{1}^{st}$$
15	11	cv	$$setvaru$$
16	15 14	cfv	$$class{1}^{st}\left(u\right)$$
17		chom	$$class\mathrm{Hom}$$
18	5 17	cfv	$$class\mathrm{Hom}\left(r\right)$$
19	13	cv	$$setvarv$$
20	19 14	cfv	$$class{1}^{st}\left(v\right)$$
21	16 20 18	co	$$class\left(1^{st}\left(u\right)\mathrm{Hom}\left(r\right)1^{st}\left(v\right)\right)$$
22		c2nd	$$class{2}^{nd}$$
23	15 22	cfv	$$class{2}^{nd}\left(u\right)$$
24	7 17	cfv	$$class\mathrm{Hom}\left(s\right)$$
25	19 22	cfv	$$class{2}^{nd}\left(v\right)$$
26	23 25 24	co	$$class\left(2^{nd}\left(u\right)\mathrm{Hom}\left(s\right)2^{nd}\left(v\right)\right)$$
27	21 26	cxp	$$class\left(\left(1^{st}\left(u\right)\mathrm{Hom}\left(r\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(s\right)2^{nd}\left(v\right)\right)\right)$$
28	11 13 12 12 27	cmpo	$$class\left(u\in b,v\in b⟼\left(1^{st}\left(u\right)\mathrm{Hom}\left(r\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(s\right)2^{nd}\left(v\right)\right)\right)$$
29		vh	$$setvarh$$
30		cnx	$$class\mathrm{ndx}$$
31	30 4	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
32	31 12	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩$$
33	30 17	cfv	$$class\mathrm{Hom}\left(\mathrm{ndx}\right)$$
34	29	cv	$$setvarh$$
35	33 34	cop	$$class⟨\mathrm{Hom}\left(\mathrm{ndx}\right),h⟩$$
36		cco	$$class\mathrm{comp}$$
37	30 36	cfv	$$class\mathrm{comp}\left(\mathrm{ndx}\right)$$
38		vx	$$setvarx$$
39	12 12	cxp	$$class\left(b\times b\right)$$
40		vy	$$setvary$$
41		vg	$$setvarg$$
42	38	cv	$$setvarx$$
43	42 22	cfv	$$class{2}^{nd}\left(x\right)$$
44	40	cv	$$setvary$$
45	43 44 34	co	$$class\left(2^{nd}\left(x\right)hy\right)$$
46		vf	$$setvarf$$
47	42 34	cfv	$$classh\left(x\right)$$
48	41	cv	$$setvarg$$
49	48 14	cfv	$$class{1}^{st}\left(g\right)$$
50	42 14	cfv	$$class{1}^{st}\left(x\right)$$
51	50 14	cfv	$$class{1}^{st}\left(1^{st}\left(x\right)\right)$$
52	43 14	cfv	$$class{1}^{st}\left(2^{nd}\left(x\right)\right)$$
53	51 52	cop	$$class⟨1^{st}\left(1^{st}\left(x\right)\right),1^{st}\left(2^{nd}\left(x\right)\right)⟩$$
54	5 36	cfv	$$class\mathrm{comp}\left(r\right)$$
55	44 14	cfv	$$class{1}^{st}\left(y\right)$$
56	53 55 54	co	$$class\left(⟨1^{st}\left(1^{st}\left(x\right)\right),1^{st}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(r\right)1^{st}\left(y\right)\right)$$
57	46	cv	$$setvarf$$
58	57 14	cfv	$$class{1}^{st}\left(f\right)$$
59	49 58 56	co	$$class\left(1^{st}\left(g\right)\left(⟨1^{st}\left(1^{st}\left(x\right)\right),1^{st}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(r\right)1^{st}\left(y\right)\right)1^{st}\left(f\right)\right)$$
60	48 22	cfv	$$class{2}^{nd}\left(g\right)$$
61	50 22	cfv	$$class{2}^{nd}\left(1^{st}\left(x\right)\right)$$
62	43 22	cfv	$$class{2}^{nd}\left(2^{nd}\left(x\right)\right)$$
63	61 62	cop	$$class⟨2^{nd}\left(1^{st}\left(x\right)\right),2^{nd}\left(2^{nd}\left(x\right)\right)⟩$$
64	7 36	cfv	$$class\mathrm{comp}\left(s\right)$$
65	44 22	cfv	$$class{2}^{nd}\left(y\right)$$
66	63 65 64	co	$$class\left(⟨2^{nd}\left(1^{st}\left(x\right)\right),2^{nd}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(s\right)2^{nd}\left(y\right)\right)$$
67	57 22	cfv	$$class{2}^{nd}\left(f\right)$$
68	60 67 66	co	$$class\left(2^{nd}\left(g\right)\left(⟨2^{nd}\left(1^{st}\left(x\right)\right),2^{nd}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(s\right)2^{nd}\left(y\right)\right)2^{nd}\left(f\right)\right)$$
69	59 68	cop	$$class⟨1^{st}\left(g\right)\left(⟨1^{st}\left(1^{st}\left(x\right)\right),1^{st}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(r\right)1^{st}\left(y\right)\right)1^{st}\left(f\right),2^{nd}\left(g\right)\left(⟨2^{nd}\left(1^{st}\left(x\right)\right),2^{nd}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(s\right)2^{nd}\left(y\right)\right)2^{nd}\left(f\right)⟩$$
70	41 46 45 47 69	cmpo	$$class\left(g\in \left(2^{nd}\left(x\right)hy\right),f\in h\left(x\right)⟼⟨1^{st}\left(g\right)\left(⟨1^{st}\left(1^{st}\left(x\right)\right),1^{st}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(r\right)1^{st}\left(y\right)\right)1^{st}\left(f\right),2^{nd}\left(g\right)\left(⟨2^{nd}\left(1^{st}\left(x\right)\right),2^{nd}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(s\right)2^{nd}\left(y\right)\right)2^{nd}\left(f\right)⟩\right)$$
71	38 40 39 12 70	cmpo	$$class\left(x\in \left(b\times b\right),y\in b⟼\left(g\in \left(2^{nd}\left(x\right)hy\right),f\in h\left(x\right)⟼⟨1^{st}\left(g\right)\left(⟨1^{st}\left(1^{st}\left(x\right)\right),1^{st}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(r\right)1^{st}\left(y\right)\right)1^{st}\left(f\right),2^{nd}\left(g\right)\left(⟨2^{nd}\left(1^{st}\left(x\right)\right),2^{nd}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(s\right)2^{nd}\left(y\right)\right)2^{nd}\left(f\right)⟩\right)\right)$$
72	37 71	cop	$$class⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(x\in \left(b\times b\right),y\in b⟼\left(g\in \left(2^{nd}\left(x\right)hy\right),f\in h\left(x\right)⟼⟨1^{st}\left(g\right)\left(⟨1^{st}\left(1^{st}\left(x\right)\right),1^{st}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(r\right)1^{st}\left(y\right)\right)1^{st}\left(f\right),2^{nd}\left(g\right)\left(⟨2^{nd}\left(1^{st}\left(x\right)\right),2^{nd}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(s\right)2^{nd}\left(y\right)\right)2^{nd}\left(f\right)⟩\right)\right)⟩$$
73	32 35 72	ctp	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),h⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(x\in \left(b\times b\right),y\in b⟼\left(g\in \left(2^{nd}\left(x\right)hy\right),f\in h\left(x\right)⟼⟨1^{st}\left(g\right)\left(⟨1^{st}\left(1^{st}\left(x\right)\right),1^{st}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(r\right)1^{st}\left(y\right)\right)1^{st}\left(f\right),2^{nd}\left(g\right)\left(⟨2^{nd}\left(1^{st}\left(x\right)\right),2^{nd}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(s\right)2^{nd}\left(y\right)\right)2^{nd}\left(f\right)⟩\right)\right)⟩\right\}$$
74	29 28 73	csb	$$class⦋\left(u\in b,v\in b⟼\left(1^{st}\left(u\right)\mathrm{Hom}\left(r\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(s\right)2^{nd}\left(v\right)\right)\right)/h⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),h⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(x\in \left(b\times b\right),y\in b⟼\left(g\in \left(2^{nd}\left(x\right)hy\right),f\in h\left(x\right)⟼⟨1^{st}\left(g\right)\left(⟨1^{st}\left(1^{st}\left(x\right)\right),1^{st}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(r\right)1^{st}\left(y\right)\right)1^{st}\left(f\right),2^{nd}\left(g\right)\left(⟨2^{nd}\left(1^{st}\left(x\right)\right),2^{nd}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(s\right)2^{nd}\left(y\right)\right)2^{nd}\left(f\right)⟩\right)\right)⟩\right\}$$
75	10 9 74	csb	$$class⦋\left({\mathrm{Base}}_r\times {\mathrm{Base}}_s\right)/b⦌⦋\left(u\in b,v\in b⟼\left(1^{st}\left(u\right)\mathrm{Hom}\left(r\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(s\right)2^{nd}\left(v\right)\right)\right)/h⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),h⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(x\in \left(b\times b\right),y\in b⟼\left(g\in \left(2^{nd}\left(x\right)hy\right),f\in h\left(x\right)⟼⟨1^{st}\left(g\right)\left(⟨1^{st}\left(1^{st}\left(x\right)\right),1^{st}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(r\right)1^{st}\left(y\right)\right)1^{st}\left(f\right),2^{nd}\left(g\right)\left(⟨2^{nd}\left(1^{st}\left(x\right)\right),2^{nd}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(s\right)2^{nd}\left(y\right)\right)2^{nd}\left(f\right)⟩\right)\right)⟩\right\}$$
76	1 3 2 2 75	cmpo	$$class\left(r\in \mathrm{V},s\in \mathrm{V}⟼⦋\left({\mathrm{Base}}_r\times {\mathrm{Base}}_s\right)/b⦌⦋\left(u\in b,v\in b⟼\left(1^{st}\left(u\right)\mathrm{Hom}\left(r\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(s\right)2^{nd}\left(v\right)\right)\right)/h⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),h⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(x\in \left(b\times b\right),y\in b⟼\left(g\in \left(2^{nd}\left(x\right)hy\right),f\in h\left(x\right)⟼⟨1^{st}\left(g\right)\left(⟨1^{st}\left(1^{st}\left(x\right)\right),1^{st}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(r\right)1^{st}\left(y\right)\right)1^{st}\left(f\right),2^{nd}\left(g\right)\left(⟨2^{nd}\left(1^{st}\left(x\right)\right),2^{nd}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(s\right)2^{nd}\left(y\right)\right)2^{nd}\left(f\right)⟩\right)\right)⟩\right\}\right)$$
77	0 76	wceq	$$wff{\times }_c=\left(r\in \mathrm{V},s\in \mathrm{V}⟼⦋\left({\mathrm{Base}}_r\times {\mathrm{Base}}_s\right)/b⦌⦋\left(u\in b,v\in b⟼\left(1^{st}\left(u\right)\mathrm{Hom}\left(r\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(s\right)2^{nd}\left(v\right)\right)\right)/h⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),h⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(x\in \left(b\times b\right),y\in b⟼\left(g\in \left(2^{nd}\left(x\right)hy\right),f\in h\left(x\right)⟼⟨1^{st}\left(g\right)\left(⟨1^{st}\left(1^{st}\left(x\right)\right),1^{st}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(r\right)1^{st}\left(y\right)\right)1^{st}\left(f\right),2^{nd}\left(g\right)\left(⟨2^{nd}\left(1^{st}\left(x\right)\right),2^{nd}\left(2^{nd}\left(x\right)\right)⟩\mathrm{comp}\left(s\right)2^{nd}\left(y\right)\right)2^{nd}\left(f\right)⟩\right)\right)⟩\right\}\right)$$