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 18060

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 18056	. 2 class ×_c
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 3445	. . 3 class V
5		vb	. . . 4 setvar 𝑏
6	2	cv 1540	. . . . . 6 class 𝑟
7		cbs 17083	. . . . . 6 class Base
8	6, 7	cfv 6496	. . . . 5 class (Base‘𝑟)
9	3	cv 1540	. . . . . 6 class 𝑠
10	9, 7	cfv 6496	. . . . 5 class (Base‘𝑠)
11	8, 10	cxp 5631	. . . 4 class ((Base‘𝑟) × (Base‘𝑠))
12		vh	. . . . 5 setvar ℎ
13		vu	. . . . . 6 setvar 𝑢
14		vv	. . . . . 6 setvar 𝑣
15	5	cv 1540	. . . . . 6 class 𝑏
16	13	cv 1540	. . . . . . . . 9 class 𝑢
17		c1st 7919	. . . . . . . . 9 class 1^st
18	16, 17	cfv 6496	. . . . . . . 8 class (1^st ‘𝑢)
19	14	cv 1540	. . . . . . . . 9 class 𝑣
20	19, 17	cfv 6496	. . . . . . . 8 class (1^st ‘𝑣)
21		chom 17144	. . . . . . . . 9 class Hom
22	6, 21	cfv 6496	. . . . . . . 8 class (Hom ‘𝑟)
23	18, 20, 22	co 7357	. . . . . . 7 class ((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣))
24		c2nd 7920	. . . . . . . . 9 class 2^nd
25	16, 24	cfv 6496	. . . . . . . 8 class (2^nd ‘𝑢)
26	19, 24	cfv 6496	. . . . . . . 8 class (2^nd ‘𝑣)
27	9, 21	cfv 6496	. . . . . . . 8 class (Hom ‘𝑠)
28	25, 26, 27	co 7357	. . . . . . 7 class ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣))
29	23, 28	cxp 5631	. . . . . 6 class (((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣)))
30	13, 14, 15, 15, 29	cmpo 7359	. . . . 5 class (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^st ‘𝑢)(Hom ‘𝑟)(1^st ‘𝑣)) × ((2^nd ‘𝑢)(Hom ‘𝑠)(2^nd ‘𝑣))))
31		cnx 17065	. . . . . . . 8 class ndx
32	31, 7	cfv 6496	. . . . . . 7 class (Base‘ndx)
33	32, 15	cop 4592	. . . . . 6 class ⟨(Base‘ndx), 𝑏⟩
34	31, 21	cfv 6496	. . . . . . 7 class (Hom ‘ndx)
35	12	cv 1540	. . . . . . 7 class ℎ
36	34, 35	cop 4592	. . . . . 6 class ⟨(Hom ‘ndx), ℎ⟩
37		cco 17145	. . . . . . . 8 class comp
38	31, 37	cfv 6496	. . . . . . 7 class (comp‘ndx)
39		vx	. . . . . . . 8 setvar 𝑥
40		vy	. . . . . . . 8 setvar 𝑦
41	15, 15	cxp 5631	. . . . . . . 8 class (𝑏 × 𝑏)
42		vg	. . . . . . . . 9 setvar 𝑔
43		vf	. . . . . . . . 9 setvar 𝑓
44	39	cv 1540	. . . . . . . . . . 11 class 𝑥
45	44, 24	cfv 6496	. . . . . . . . . 10 class (2^nd ‘𝑥)
46	40	cv 1540	. . . . . . . . . 10 class 𝑦
47	45, 46, 35	co 7357	. . . . . . . . 9 class ((2^nd ‘𝑥)ℎ𝑦)
48	44, 35	cfv 6496	. . . . . . . . 9 class (ℎ‘𝑥)
49	42	cv 1540	. . . . . . . . . . . 12 class 𝑔
50	49, 17	cfv 6496	. . . . . . . . . . 11 class (1^st ‘𝑔)
51	43	cv 1540	. . . . . . . . . . . 12 class 𝑓
52	51, 17	cfv 6496	. . . . . . . . . . 11 class (1^st ‘𝑓)
53	44, 17	cfv 6496	. . . . . . . . . . . . . 14 class (1^st ‘𝑥)
54	53, 17	cfv 6496	. . . . . . . . . . . . 13 class (1^st ‘(1^st ‘𝑥))
55	45, 17	cfv 6496	. . . . . . . . . . . . 13 class (1^st ‘(2^nd ‘𝑥))
56	54, 55	cop 4592	. . . . . . . . . . . 12 class ⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩
57	46, 17	cfv 6496	. . . . . . . . . . . 12 class (1^st ‘𝑦)
58	6, 37	cfv 6496	. . . . . . . . . . . 12 class (comp‘𝑟)
59	56, 57, 58	co 7357	. . . . . . . . . . 11 class (⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩(comp‘𝑟)(1^st ‘𝑦))
60	50, 52, 59	co 7357	. . . . . . . . . 10 class ((1^st ‘𝑔)(⟨(1^st ‘(1^st ‘𝑥)), (1^st ‘(2^nd ‘𝑥))⟩(comp‘𝑟)(1^st ‘𝑦))(1^st ‘𝑓))
61	49, 24	cfv 6496	. . . . . . . . . . 11 class (2^nd ‘𝑔)
62	51, 24	cfv 6496	. . . . . . . . . . 11 class (2^nd ‘𝑓)
63	53, 24	cfv 6496	. . . . . . . . . . . . 13 class (2^nd ‘(1^st ‘𝑥))
64	45, 24	cfv 6496	. . . . . . . . . . . . 13 class (2^nd ‘(2^nd ‘𝑥))
65	63, 64	cop 4592	. . . . . . . . . . . 12 class ⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩
66	46, 24	cfv 6496	. . . . . . . . . . . 12 class (2^nd ‘𝑦)
67	9, 37	cfv 6496	. . . . . . . . . . . 12 class (comp‘𝑠)
68	65, 66, 67	co 7357	. . . . . . . . . . 11 class (⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))
69	61, 62, 68	co 7357	. . . . . . . . . 10 class ((2^nd ‘𝑔)(⟨(2^nd ‘(1^st ‘𝑥)), (2^nd ‘(2^nd ‘𝑥))⟩(comp‘𝑠)(2^nd ‘𝑦))(2^nd ‘𝑓))
70	60, 69	cop 4592	. . . . . . . . 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 7359	. . . . . . . 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 7359	. . . . . . 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 4592	. . . . . 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 4590	. . . . 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 3855	. . . 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 3855	. . 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 7359	. 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 1541	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 18064 xpcval 18065

W3C validator