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} = (r \in V, s \in V ⟼ ⦋ ({Base}_{r} \times {Base}_{s}) / b ⦌ ⦋ (u \in b, v \in b ⟼ (1^{st} (u) Hom (r) 1^{st} (v)) \times (2^{nd} (u) Hom (s) 2^{nd} (v))) / h ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨Hom (ndx), h⟩, ⟨comp (ndx), (x \in (b \times b), y \in b ⟼ (g \in (2^{nd} (x) h y), f \in h (x) ⟼ ⟨1^{st} (g) (⟨1^{st} (1^{st} (x)), 1^{st} (2^{nd} (x))⟩ comp (r) 1^{st} (y)) 1^{st} (f), 2^{nd} (g) (⟨2^{nd} (1^{st} (x)), 2^{nd} (2^{nd} (x))⟩ comp (s) 2^{nd} (y)) 2^{nd} (f)⟩))⟩\})$

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-xpc

Detailed syntax breakdown