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 18184

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 18180	. 2 class ×_c
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 3459	. . 3 class V
5		vb	. . . 4 setvar 𝑏
6	2	cv 1539	. . . . . 6 class 𝑟
7		cbs 17228	. . . . . 6 class Base
8	6, 7	cfv 6531	. . . . 5 class (Base‘𝑟)
9	3	cv 1539	. . . . . 6 class 𝑠
10	9, 7	cfv 6531	. . . . 5 class (Base‘𝑠)
11	8, 10	cxp 5652	. . . 4 class ((Base‘𝑟) × (Base‘𝑠))
12		vh	. . . . 5 setvar ℎ
13		vu	. . . . . 6 setvar 𝑢
14		vv	. . . . . 6 setvar 𝑣
15	5	cv 1539	. . . . . 6 class 𝑏
16	13	cv 1539	. . . . . . . . 9 class 𝑢
17		c1st 7986	. . . . . . . . 9 class 1^st
18	16, 17	cfv 6531	. . . . . . . 8 class (1^st ‘𝑢)
19	14	cv 1539	. . . . . . . . 9 class 𝑣
20	19, 17	cfv 6531	. . . . . . . 8 class (1^st ‘𝑣)
21		chom 17282	. . . . . . . . 9 class Hom
22	6, 21	cfv 6531	. . . . . . . 8 class (Hom ‘𝑟)
23	18, 20, 22	co 7405	. . . . . . 7 class ((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣))
24		c2nd 7987	. . . . . . . . 9 class 2^nd
25	16, 24	cfv 6531	. . . . . . . 8 class (2^nd ‘𝑢)
26	19, 24	cfv 6531	. . . . . . . 8 class (2^nd ‘𝑣)
27	9, 21	cfv 6531	. . . . . . . 8 class (Hom ‘𝑠)
28	25, 26, 27	co 7405	. . . . . . 7 class ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣))
29	23, 28	cxp 5652	. . . . . 6 class (((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣)))
30	13, 14, 15, 15, 29	cmpo 7407	. . . . 5 class (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣))))
31		cnx 17212	. . . . . . . 8 class ndx
32	31, 7	cfv 6531	. . . . . . 7 class (Base‘ndx)
33	32, 15	cop 4607	. . . . . 6 class ⟨(Base‘ndx), 𝑏⟩
34	31, 21	cfv 6531	. . . . . . 7 class (Hom ‘ndx)
35	12	cv 1539	. . . . . . 7 class ℎ
36	34, 35	cop 4607	. . . . . 6 class ⟨(Hom ‘ndx), ℎ⟩
37		cco 17283	. . . . . . . 8 class comp
38	31, 37	cfv 6531	. . . . . . 7 class (comp‘ndx)
39		vx	. . . . . . . 8 setvar 𝑥
40		vy	. . . . . . . 8 setvar 𝑦
41	15, 15	cxp 5652	. . . . . . . 8 class (𝑏 × 𝑏)
42		vg	. . . . . . . . 9 setvar 𝑔
43		vf	. . . . . . . . 9 setvar 𝑓
44	39	cv 1539	. . . . . . . . . . 11 class 𝑥
45	44, 24	cfv 6531	. . . . . . . . . 10 class (2^nd ‘𝑥)
46	40	cv 1539	. . . . . . . . . 10 class 𝑦
47	45, 46, 35	co 7405	. . . . . . . . 9 class ((2^nd ‘𝑥)ℎ𝑦)
48	44, 35	cfv 6531	. . . . . . . . 9 class (ℎ‘𝑥)
49	42	cv 1539	. . . . . . . . . . . 12 class 𝑔
50	49, 17	cfv 6531	. . . . . . . . . . 11 class (1^st ‘𝑔)
51	43	cv 1539	. . . . . . . . . . . 12 class 𝑓
52	51, 17	cfv 6531	. . . . . . . . . . 11 class (1^st ‘𝑓)
53	44, 17	cfv 6531	. . . . . . . . . . . . . 14 class (1^st ‘𝑥)
54	53, 17	cfv 6531	. . . . . . . . . . . . 13 class (1^st ‘(1^st ‘𝑥))
55	45, 17	cfv 6531	. . . . . . . . . . . . 13 class (1^st ‘(2^nd ‘𝑥))
56	54, 55	cop 4607	. . . . . . . . . . . 12 class ⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩
57	46, 17	cfv 6531	. . . . . . . . . . . 12 class (1^st ‘𝑦)
58	6, 37	cfv 6531	. . . . . . . . . . . 12 class (comp‘𝑟)
59	56, 57, 58	co 7405	. . . . . . . . . . 11 class (⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩(comp‘𝑟)(1^st ‘𝑦))
60	50, 52, 59	co 7405	. . . . . . . . . 10 class ((1^st ‘𝑔)(⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩(comp‘𝑟)(1^st ‘𝑦))(1^st ‘𝑓))
61	49, 24	cfv 6531	. . . . . . . . . . 11 class (2^nd ‘𝑔)
62	51, 24	cfv 6531	. . . . . . . . . . 11 class (2^nd ‘𝑓)
63	53, 24	cfv 6531	. . . . . . . . . . . . 13 class (2^nd ‘(1^st ‘𝑥))
64	45, 24	cfv 6531	. . . . . . . . . . . . 13 class (2^nd ‘(2^nd ‘𝑥))
65	63, 64	cop 4607	. . . . . . . . . . . 12 class ⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩
66	46, 24	cfv 6531	. . . . . . . . . . . 12 class (2^nd ‘𝑦)
67	9, 37	cfv 6531	. . . . . . . . . . . 12 class (comp‘𝑠)
68	65, 66, 67	co 7405	. . . . . . . . . . 11 class (⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))
69	61, 62, 68	co 7405	. . . . . . . . . 10 class ((2^nd ‘𝑔)(⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))(2^nd ‘𝑓))
70	60, 69	cop 4607	. . . . . . . . 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 7407	. . . . . . . 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 7407	. . . . . . 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 4607	. . . . . 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 4605	. . . . 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 3874	. . . 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 3874	. . 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 7407	. 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 1540	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 18188 xpcval 18189 reldmxpcALT 49164

W3C validator