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 18351

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 18347	. 2 class ×_c
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 3450	. . 3 class V
5		vb	. . . 4 setvar 𝑏
6	2	cv 1568	. . . . . 6 class 𝑟
7		cbs 17392	. . . . . 6 class Base
8	6, 7	cfv 6538	. . . . 5 class (Base‘𝑟)
9	3	cv 1568	. . . . . 6 class 𝑠
10	9, 7	cfv 6538	. . . . 5 class (Base‘𝑠)
11	8, 10	cxp 5648	. . . 4 class ((Base‘𝑟) × (Base‘𝑠))
12		vh	. . . . 5 setvar ℎ
13		vu	. . . . . 6 setvar 𝑢
14		vv	. . . . . 6 setvar 𝑣
15	5	cv 1568	. . . . . 6 class 𝑏
16	13	cv 1568	. . . . . . . . 9 class 𝑢
17		c1st 7999	. . . . . . . . 9 class 1^st
18	16, 17	cfv 6538	. . . . . . . 8 class (1^st ‘𝑢)
19	14	cv 1568	. . . . . . . . 9 class 𝑣
20	19, 17	cfv 6538	. . . . . . . 8 class (1^st ‘𝑣)
21		chom 17444	. . . . . . . . 9 class Hom
22	6, 21	cfv 6538	. . . . . . . 8 class (Hom ‘𝑟)
23	18, 20, 22	co 7420	. . . . . . 7 class ((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣))
24		c2nd 8000	. . . . . . . . 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 7420	. . . . . . 7 class ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣))
29	23, 28	cxp 5648	. . . . . 6 class (((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣)))
30	13, 14, 15, 15, 29	cmpo 7422	. . . . 5 class (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣))))
31		cnx 17376	. . . . . . . 8 class ndx
32	31, 7	cfv 6538	. . . . . . 7 class (Base‘ndx)
33	32, 15	cop 4834	. . . . . 6 class ⟨(Base‘ndx), 𝑏⟩
34	31, 21	cfv 6538	. . . . . . 7 class (Hom ‘ndx)
35	12	cv 1568	. . . . . . 7 class ℎ
36	34, 35	cop 4834	. . . . . 6 class ⟨(Hom ‘ndx), ℎ⟩
37		cco 17445	. . . . . . . 8 class comp
38	31, 37	cfv 6538	. . . . . . 7 class (comp‘ndx)
39		vx	. . . . . . . 8 setvar 𝑥
40		vy	. . . . . . . 8 setvar 𝑦
41	15, 15	cxp 5648	. . . . . . . 8 class (𝑏 × 𝑏)
42		vg	. . . . . . . . 9 setvar 𝑔
43		vf	. . . . . . . . 9 setvar 𝑓
44	39	cv 1568	. . . . . . . . . . 11 class 𝑥
45	44, 24	cfv 6538	. . . . . . . . . 10 class (2^nd ‘𝑥)
46	40	cv 1568	. . . . . . . . . 10 class 𝑦
47	45, 46, 35	co 7420	. . . . . . . . 9 class ((2^nd ‘𝑥)ℎ𝑦)
48	44, 35	cfv 6538	. . . . . . . . 9 class (ℎ‘𝑥)
49	42	cv 1568	. . . . . . . . . . . 12 class 𝑔
50	49, 17	cfv 6538	. . . . . . . . . . 11 class (1^st ‘𝑔)
51	43	cv 1568	. . . . . . . . . . . 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 4834	. . . . . . . . . . . 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 7420	. . . . . . . . . . 11 class (⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩(comp‘𝑟)(1^st ‘𝑦))
60	50, 52, 59	co 7420	. . . . . . . . . 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 4834	. . . . . . . . . . . 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 7420	. . . . . . . . . . 11 class (⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))
69	61, 62, 68	co 7420	. . . . . . . . . 10 class ((2^nd ‘𝑔)(⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))(2^nd ‘𝑓))
70	60, 69	cop 4834	. . . . . . . . 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 7422	. . . . . . . 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 7422	. . . . . . 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 4834	. . . . . 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 4588	. . . . 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 3846	. . . 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 3846	. . 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 7422	. 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 1569	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 used by: fnxpc 18355 xpcval 18356 reldmxpcALT 50462

W3C validator