df-xpc - Metamath Proof Explorer

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

Definition df-xpc 18229

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 = (𝑟 ∈ V, 𝑠 ∈ V ↦ ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣)))) / ℎ⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^st ‘𝑔)(⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩(comp‘𝑟)(1^st ‘𝑦))(1^st ‘𝑓)), ((2^nd ‘𝑔)(⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))(2^nd ‘𝑓))⟩))⟩})

Distinct variable group: 𝑓,𝑏,𝑔,ℎ,𝑟,𝑠,𝑢,𝑣,𝑥,𝑦

**Detailed syntax breakdown of Definition df-xpc**
Step	Hyp	Ref	Expression
1		cxpc 18225	. 2 class ×_c
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 3455	. . 3 class V
5		vb	. . . 4 setvar 𝑏
6	2	cv 1569	. . . . . 6 class 𝑟
7		cbs 17270	. . . . . 6 class Base
8	6, 7	cfv 6538	. . . . 5 class (Base‘𝑟)
9	3	cv 1569	. . . . . 6 class 𝑠
10	9, 7	cfv 6538	. . . . 5 class (Base‘𝑠)
11	8, 10	cxp 5661	. . . 4 class ((Base‘𝑟) × (Base‘𝑠))
12		vh	. . . . 5 setvar ℎ
13		vu	. . . . . 6 setvar 𝑢
14		vv	. . . . . 6 setvar 𝑣
15	5	cv 1569	. . . . . 6 class 𝑏
16	13	cv 1569	. . . . . . . . 9 class 𝑢
17		c1st 7985	. . . . . . . . 9 class 1^st
18	16, 17	cfv 6538	. . . . . . . 8 class (1^st ‘𝑢)
19	14	cv 1569	. . . . . . . . 9 class 𝑣
20	19, 17	cfv 6538	. . . . . . . 8 class (1^st ‘𝑣)
21		chom 17322	. . . . . . . . 9 class Hom
22	6, 21	cfv 6538	. . . . . . . 8 class (Hom ‘𝑟)
23	18, 20, 22	co 7412	. . . . . . 7 class ((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣))
24		c2nd 7986	. . . . . . . . 9 class 2^nd
25	16, 24	cfv 6538	. . . . . . . 8 class (2^nd ‘𝑢)
26	19, 24	cfv 6538	. . . . . . . 8 class (2^nd ‘𝑣)
27	9, 21	cfv 6538	. . . . . . . 8 class (Hom ‘𝑠)
28	25, 26, 27	co 7412	. . . . . . 7 class ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣))
29	23, 28	cxp 5661	. . . . . 6 class (((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣)))
30	13, 14, 15, 15, 29	cmpo 7414	. . . . 5 class (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣))))
31		cnx 17254	. . . . . . . 8 class ndx
32	31, 7	cfv 6538	. . . . . . 7 class (Base‘ndx)
33	32, 15	cop 4596	. . . . . 6 class ⟨(Base‘ndx), 𝑏⟩
34	31, 21	cfv 6538	. . . . . . 7 class (Hom ‘ndx)
35	12	cv 1569	. . . . . . 7 class ℎ
36	34, 35	cop 4596	. . . . . 6 class ⟨(Hom ‘ndx), ℎ⟩
37		cco 17323	. . . . . . . 8 class comp
38	31, 37	cfv 6538	. . . . . . 7 class (comp‘ndx)
39		vx	. . . . . . . 8 setvar 𝑥
40		vy	. . . . . . . 8 setvar 𝑦
41	15, 15	cxp 5661	. . . . . . . 8 class (𝑏 × 𝑏)
42		vg	. . . . . . . . 9 setvar 𝑔
43		vf	. . . . . . . . 9 setvar 𝑓
44	39	cv 1569	. . . . . . . . . . 11 class 𝑥
45	44, 24	cfv 6538	. . . . . . . . . 10 class (2^nd ‘𝑥)
46	40	cv 1569	. . . . . . . . . 10 class 𝑦
47	45, 46, 35	co 7412	. . . . . . . . 9 class ((2^nd ‘𝑥)ℎ𝑦)
48	44, 35	cfv 6538	. . . . . . . . 9 class (ℎ‘𝑥)
49	42	cv 1569	. . . . . . . . . . . 12 class 𝑔
50	49, 17	cfv 6538	. . . . . . . . . . 11 class (1^st ‘𝑔)
51	43	cv 1569	. . . . . . . . . . . 12 class 𝑓
52	51, 17	cfv 6538	. . . . . . . . . . 11 class (1^st ‘𝑓)
53	44, 17	cfv 6538	. . . . . . . . . . . . . 14 class (1^st ‘𝑥)
54	53, 17	cfv 6538	. . . . . . . . . . . . 13 class (1^st ‘(1^st ‘𝑥))
55	45, 17	cfv 6538	. . . . . . . . . . . . 13 class (1^st ‘(2^nd ‘𝑥))
56	54, 55	cop 4596	. . . . . . . . . . . 12 class ⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩
57	46, 17	cfv 6538	. . . . . . . . . . . 12 class (1^st ‘𝑦)
58	6, 37	cfv 6538	. . . . . . . . . . . 12 class (comp‘𝑟)
59	56, 57, 58	co 7412	. . . . . . . . . . 11 class (⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩(comp‘𝑟)(1^st ‘𝑦))
60	50, 52, 59	co 7412	. . . . . . . . . 10 class ((1^st ‘𝑔)(⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩(comp‘𝑟)(1^st ‘𝑦))(1^st ‘𝑓))
61	49, 24	cfv 6538	. . . . . . . . . . 11 class (2^nd ‘𝑔)
62	51, 24	cfv 6538	. . . . . . . . . . 11 class (2^nd ‘𝑓)
63	53, 24	cfv 6538	. . . . . . . . . . . . 13 class (2^nd ‘(1^st ‘𝑥))
64	45, 24	cfv 6538	. . . . . . . . . . . . 13 class (2^nd ‘(2^nd ‘𝑥))
65	63, 64	cop 4596	. . . . . . . . . . . 12 class ⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩
66	46, 24	cfv 6538	. . . . . . . . . . . 12 class (2^nd ‘𝑦)
67	9, 37	cfv 6538	. . . . . . . . . . . 12 class (comp‘𝑠)
68	65, 66, 67	co 7412	. . . . . . . . . . 11 class (⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))
69	61, 62, 68	co 7412	. . . . . . . . . 10 class ((2^nd ‘𝑔)(⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))(2^nd ‘𝑓))
70	60, 69	cop 4596	. . . . . . . . 9 class ⟨((1^st ‘𝑔)(⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩(comp‘𝑟)(1^st ‘𝑦))(1^st ‘𝑓)), ((2^nd ‘𝑔)(⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))(2^nd ‘𝑓))⟩
71	42, 43, 47, 48, 70	cmpo 7414	. . . . . . . 8 class (𝑔 ∈ ((2^nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^st ‘𝑔)(⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩(comp‘𝑟)(1^st ‘𝑦))(1^st ‘𝑓)), ((2^nd ‘𝑔)(⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))(2^nd ‘𝑓))⟩)
72	39, 40, 41, 15, 71	cmpo 7414	. . . . . . 7 class (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^st ‘𝑔)(⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩(comp‘𝑟)(1^st ‘𝑦))(1^st ‘𝑓)), ((2^nd ‘𝑔)(⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))(2^nd ‘𝑓))⟩))
73	38, 72	cop 4596	. . . . . 6 class ⟨(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^st ‘𝑔)(⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩(comp‘𝑟)(1^st ‘𝑦))(1^st ‘𝑓)), ((2^nd ‘𝑔)(⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))(2^nd ‘𝑓))⟩))⟩
74	33, 36, 73	ctp 4594	. . . . 5 class {⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^st ‘𝑔)(⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩(comp‘𝑟)(1^st ‘𝑦))(1^st ‘𝑓)), ((2^nd ‘𝑔)(⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))(2^nd ‘𝑓))⟩))⟩}
75	12, 30, 74	csb 3854	. . . 4 class ⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣)))) / ℎ⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^st ‘𝑔)(⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩(comp‘𝑟)(1^st ‘𝑦))(1^st ‘𝑓)), ((2^nd ‘𝑔)(⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))(2^nd ‘𝑓))⟩))⟩}
76	5, 11, 75	csb 3854	. . 3 class ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣)))) / ℎ⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^st ‘𝑔)(⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩(comp‘𝑟)(1^st ‘𝑦))(1^st ‘𝑓)), ((2^nd ‘𝑔)(⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))(2^nd ‘𝑓))⟩))⟩}
77	2, 3, 4, 4, 76	cmpo 7414	. 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣)))) / ℎ⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^st ‘𝑔)(⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩(comp‘𝑟)(1^st ‘𝑦))(1^st ‘𝑓)), ((2^nd ‘𝑔)(⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))(2^nd ‘𝑓))⟩))⟩})
78	1, 77	wceq 1570	1 wff ×_c = (𝑟 ∈ V, 𝑠 ∈ V ↦ ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣)))) / ℎ⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^st ‘𝑔)(⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩(comp‘𝑟)(1^st ‘𝑦))(1^st ‘𝑓)), ((2^nd ‘𝑔)(⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))(2^nd ‘𝑓))⟩))⟩})

Colors of variables: wff setvar class

This definition is referenced by: fnxpc 18233 xpcval 18234 reldmxpcALT 50008

W3C validator