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 17414

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 17410	. 2 class ×_c
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 3441	. . 3 class V
5		vb	. . . 4 setvar 𝑏
6	2	cv 1537	. . . . . 6 class 𝑟
7		cbs 16475	. . . . . 6 class Base
8	6, 7	cfv 6324	. . . . 5 class (Base‘𝑟)
9	3	cv 1537	. . . . . 6 class 𝑠
10	9, 7	cfv 6324	. . . . 5 class (Base‘𝑠)
11	8, 10	cxp 5517	. . . 4 class ((Base‘𝑟) × (Base‘𝑠))
12		vh	. . . . 5 setvar ℎ
13		vu	. . . . . 6 setvar 𝑢
14		vv	. . . . . 6 setvar 𝑣
15	5	cv 1537	. . . . . 6 class 𝑏
16	13	cv 1537	. . . . . . . . 9 class 𝑢
17		c1st 7669	. . . . . . . . 9 class 1^st
18	16, 17	cfv 6324	. . . . . . . 8 class (1^st ‘𝑢)
19	14	cv 1537	. . . . . . . . 9 class 𝑣
20	19, 17	cfv 6324	. . . . . . . 8 class (1^st ‘𝑣)
21		chom 16568	. . . . . . . . 9 class Hom
22	6, 21	cfv 6324	. . . . . . . 8 class (Hom ‘𝑟)
23	18, 20, 22	co 7135	. . . . . . 7 class ((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣))
24		c2nd 7670	. . . . . . . . 9 class 2^nd
25	16, 24	cfv 6324	. . . . . . . 8 class (2^nd ‘𝑢)
26	19, 24	cfv 6324	. . . . . . . 8 class (2^nd ‘𝑣)
27	9, 21	cfv 6324	. . . . . . . 8 class (Hom ‘𝑠)
28	25, 26, 27	co 7135	. . . . . . 7 class ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣))
29	23, 28	cxp 5517	. . . . . 6 class (((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣)))
30	13, 14, 15, 15, 29	cmpo 7137	. . . . 5 class (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣))))
31		cnx 16472	. . . . . . . 8 class ndx
32	31, 7	cfv 6324	. . . . . . 7 class (Base‘ndx)
33	32, 15	cop 4531	. . . . . 6 class ⟨(Base‘ndx), 𝑏⟩
34	31, 21	cfv 6324	. . . . . . 7 class (Hom ‘ndx)
35	12	cv 1537	. . . . . . 7 class ℎ
36	34, 35	cop 4531	. . . . . 6 class ⟨(Hom ‘ndx), ℎ⟩
37		cco 16569	. . . . . . . 8 class comp
38	31, 37	cfv 6324	. . . . . . 7 class (comp‘ndx)
39		vx	. . . . . . . 8 setvar 𝑥
40		vy	. . . . . . . 8 setvar 𝑦
41	15, 15	cxp 5517	. . . . . . . 8 class (𝑏 × 𝑏)
42		vg	. . . . . . . . 9 setvar 𝑔
43		vf	. . . . . . . . 9 setvar 𝑓
44	39	cv 1537	. . . . . . . . . . 11 class 𝑥
45	44, 24	cfv 6324	. . . . . . . . . 10 class (2^nd ‘𝑥)
46	40	cv 1537	. . . . . . . . . 10 class 𝑦
47	45, 46, 35	co 7135	. . . . . . . . 9 class ((2^nd ‘𝑥)ℎ𝑦)
48	44, 35	cfv 6324	. . . . . . . . 9 class (ℎ‘𝑥)
49	42	cv 1537	. . . . . . . . . . . 12 class 𝑔
50	49, 17	cfv 6324	. . . . . . . . . . 11 class (1^st ‘𝑔)
51	43	cv 1537	. . . . . . . . . . . 12 class 𝑓
52	51, 17	cfv 6324	. . . . . . . . . . 11 class (1^st ‘𝑓)
53	44, 17	cfv 6324	. . . . . . . . . . . . . 14 class (1^st ‘𝑥)
54	53, 17	cfv 6324	. . . . . . . . . . . . 13 class (1^st ‘(1^st ‘𝑥))
55	45, 17	cfv 6324	. . . . . . . . . . . . 13 class (1^st ‘(2^nd ‘𝑥))
56	54, 55	cop 4531	. . . . . . . . . . . 12 class ⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩
57	46, 17	cfv 6324	. . . . . . . . . . . 12 class (1^st ‘𝑦)
58	6, 37	cfv 6324	. . . . . . . . . . . 12 class (comp‘𝑟)
59	56, 57, 58	co 7135	. . . . . . . . . . 11 class (⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩(comp‘𝑟)(1^st ‘𝑦))
60	50, 52, 59	co 7135	. . . . . . . . . 10 class ((1^st ‘𝑔)(⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩(comp‘𝑟)(1^st ‘𝑦))(1^st ‘𝑓))
61	49, 24	cfv 6324	. . . . . . . . . . 11 class (2^nd ‘𝑔)
62	51, 24	cfv 6324	. . . . . . . . . . 11 class (2^nd ‘𝑓)
63	53, 24	cfv 6324	. . . . . . . . . . . . 13 class (2^nd ‘(1^st ‘𝑥))
64	45, 24	cfv 6324	. . . . . . . . . . . . 13 class (2^nd ‘(2^nd ‘𝑥))
65	63, 64	cop 4531	. . . . . . . . . . . 12 class ⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩
66	46, 24	cfv 6324	. . . . . . . . . . . 12 class (2^nd ‘𝑦)
67	9, 37	cfv 6324	. . . . . . . . . . . 12 class (comp‘𝑠)
68	65, 66, 67	co 7135	. . . . . . . . . . 11 class (⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))
69	61, 62, 68	co 7135	. . . . . . . . . 10 class ((2^nd ‘𝑔)(⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))(2^nd ‘𝑓))
70	60, 69	cop 4531	. . . . . . . . 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 7137	. . . . . . . 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 7137	. . . . . . 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 4531	. . . . . 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 4529	. . . . 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 3828	. . . 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 3828	. . 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 7137	. 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 1538	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 17418 xpcval 17419

W3C validator