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

Definition df-xpc 18166
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‘𝑠)) / 𝑏(𝑢𝑏, 𝑣𝑏 ↦ (((1st𝑢)(Hom ‘𝑟)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑠)(2nd𝑣)))) / {⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), ⟩, ⟨(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦𝑏 ↦ (𝑔 ∈ ((2nd𝑥)𝑦), 𝑓 ∈ (𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑟)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑠)(2nd𝑦))(2nd𝑓))⟩))⟩})
Distinct variable group:   𝑓,𝑏,𝑔,,𝑟,𝑠,𝑢,𝑣,𝑥,𝑦

Detailed syntax breakdown of Definition df-xpc
StepHypRef Expression
1 cxpc 18162 . 2 class ×c
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 cvv 3461 . . 3 class V
5 vb . . . 4 setvar 𝑏
62cv 1532 . . . . . 6 class 𝑟
7 cbs 17183 . . . . . 6 class Base
86, 7cfv 6549 . . . . 5 class (Base‘𝑟)
93cv 1532 . . . . . 6 class 𝑠
109, 7cfv 6549 . . . . 5 class (Base‘𝑠)
118, 10cxp 5676 . . . 4 class ((Base‘𝑟) × (Base‘𝑠))
12 vh . . . . 5 setvar
13 vu . . . . . 6 setvar 𝑢
14 vv . . . . . 6 setvar 𝑣
155cv 1532 . . . . . 6 class 𝑏
1613cv 1532 . . . . . . . . 9 class 𝑢
17 c1st 7992 . . . . . . . . 9 class 1st
1816, 17cfv 6549 . . . . . . . 8 class (1st𝑢)
1914cv 1532 . . . . . . . . 9 class 𝑣
2019, 17cfv 6549 . . . . . . . 8 class (1st𝑣)
21 chom 17247 . . . . . . . . 9 class Hom
226, 21cfv 6549 . . . . . . . 8 class (Hom ‘𝑟)
2318, 20, 22co 7419 . . . . . . 7 class ((1st𝑢)(Hom ‘𝑟)(1st𝑣))
24 c2nd 7993 . . . . . . . . 9 class 2nd
2516, 24cfv 6549 . . . . . . . 8 class (2nd𝑢)
2619, 24cfv 6549 . . . . . . . 8 class (2nd𝑣)
279, 21cfv 6549 . . . . . . . 8 class (Hom ‘𝑠)
2825, 26, 27co 7419 . . . . . . 7 class ((2nd𝑢)(Hom ‘𝑠)(2nd𝑣))
2923, 28cxp 5676 . . . . . 6 class (((1st𝑢)(Hom ‘𝑟)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑠)(2nd𝑣)))
3013, 14, 15, 15, 29cmpo 7421 . . . . 5 class (𝑢𝑏, 𝑣𝑏 ↦ (((1st𝑢)(Hom ‘𝑟)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑠)(2nd𝑣))))
31 cnx 17165 . . . . . . . 8 class ndx
3231, 7cfv 6549 . . . . . . 7 class (Base‘ndx)
3332, 15cop 4636 . . . . . 6 class ⟨(Base‘ndx), 𝑏
3431, 21cfv 6549 . . . . . . 7 class (Hom ‘ndx)
3512cv 1532 . . . . . . 7 class
3634, 35cop 4636 . . . . . 6 class ⟨(Hom ‘ndx),
37 cco 17248 . . . . . . . 8 class comp
3831, 37cfv 6549 . . . . . . 7 class (comp‘ndx)
39 vx . . . . . . . 8 setvar 𝑥
40 vy . . . . . . . 8 setvar 𝑦
4115, 15cxp 5676 . . . . . . . 8 class (𝑏 × 𝑏)
42 vg . . . . . . . . 9 setvar 𝑔
43 vf . . . . . . . . 9 setvar 𝑓
4439cv 1532 . . . . . . . . . . 11 class 𝑥
4544, 24cfv 6549 . . . . . . . . . 10 class (2nd𝑥)
4640cv 1532 . . . . . . . . . 10 class 𝑦
4745, 46, 35co 7419 . . . . . . . . 9 class ((2nd𝑥)𝑦)
4844, 35cfv 6549 . . . . . . . . 9 class (𝑥)
4942cv 1532 . . . . . . . . . . . 12 class 𝑔
5049, 17cfv 6549 . . . . . . . . . . 11 class (1st𝑔)
5143cv 1532 . . . . . . . . . . . 12 class 𝑓
5251, 17cfv 6549 . . . . . . . . . . 11 class (1st𝑓)
5344, 17cfv 6549 . . . . . . . . . . . . . 14 class (1st𝑥)
5453, 17cfv 6549 . . . . . . . . . . . . 13 class (1st ‘(1st𝑥))
5545, 17cfv 6549 . . . . . . . . . . . . 13 class (1st ‘(2nd𝑥))
5654, 55cop 4636 . . . . . . . . . . . 12 class ⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩
5746, 17cfv 6549 . . . . . . . . . . . 12 class (1st𝑦)
586, 37cfv 6549 . . . . . . . . . . . 12 class (comp‘𝑟)
5956, 57, 58co 7419 . . . . . . . . . . 11 class (⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑟)(1st𝑦))
6050, 52, 59co 7419 . . . . . . . . . 10 class ((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑟)(1st𝑦))(1st𝑓))
6149, 24cfv 6549 . . . . . . . . . . 11 class (2nd𝑔)
6251, 24cfv 6549 . . . . . . . . . . 11 class (2nd𝑓)
6353, 24cfv 6549 . . . . . . . . . . . . 13 class (2nd ‘(1st𝑥))
6445, 24cfv 6549 . . . . . . . . . . . . 13 class (2nd ‘(2nd𝑥))
6563, 64cop 4636 . . . . . . . . . . . 12 class ⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩
6646, 24cfv 6549 . . . . . . . . . . . 12 class (2nd𝑦)
679, 37cfv 6549 . . . . . . . . . . . 12 class (comp‘𝑠)
6865, 66, 67co 7419 . . . . . . . . . . 11 class (⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑠)(2nd𝑦))
6961, 62, 68co 7419 . . . . . . . . . 10 class ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑠)(2nd𝑦))(2nd𝑓))
7060, 69cop 4636 . . . . . . . . 9 class ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑟)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑠)(2nd𝑦))(2nd𝑓))⟩
7142, 43, 47, 48, 70cmpo 7421 . . . . . . . 8 class (𝑔 ∈ ((2nd𝑥)𝑦), 𝑓 ∈ (𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑟)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑠)(2nd𝑦))(2nd𝑓))⟩)
7239, 40, 41, 15, 71cmpo 7421 . . . . . . 7 class (𝑥 ∈ (𝑏 × 𝑏), 𝑦𝑏 ↦ (𝑔 ∈ ((2nd𝑥)𝑦), 𝑓 ∈ (𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑟)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑠)(2nd𝑦))(2nd𝑓))⟩))
7338, 72cop 4636 . . . . . 6 class ⟨(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦𝑏 ↦ (𝑔 ∈ ((2nd𝑥)𝑦), 𝑓 ∈ (𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑟)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑠)(2nd𝑦))(2nd𝑓))⟩))⟩
7433, 36, 73ctp 4634 . . . . 5 class {⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), ⟩, ⟨(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦𝑏 ↦ (𝑔 ∈ ((2nd𝑥)𝑦), 𝑓 ∈ (𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑟)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑠)(2nd𝑦))(2nd𝑓))⟩))⟩}
7512, 30, 74csb 3889 . . . 4 class (𝑢𝑏, 𝑣𝑏 ↦ (((1st𝑢)(Hom ‘𝑟)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑠)(2nd𝑣)))) / {⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), ⟩, ⟨(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦𝑏 ↦ (𝑔 ∈ ((2nd𝑥)𝑦), 𝑓 ∈ (𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑟)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑠)(2nd𝑦))(2nd𝑓))⟩))⟩}
765, 11, 75csb 3889 . . 3 class ((Base‘𝑟) × (Base‘𝑠)) / 𝑏(𝑢𝑏, 𝑣𝑏 ↦ (((1st𝑢)(Hom ‘𝑟)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑠)(2nd𝑣)))) / {⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), ⟩, ⟨(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦𝑏 ↦ (𝑔 ∈ ((2nd𝑥)𝑦), 𝑓 ∈ (𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑟)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑠)(2nd𝑦))(2nd𝑓))⟩))⟩}
772, 3, 4, 4, 76cmpo 7421 . 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ ((Base‘𝑟) × (Base‘𝑠)) / 𝑏(𝑢𝑏, 𝑣𝑏 ↦ (((1st𝑢)(Hom ‘𝑟)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑠)(2nd𝑣)))) / {⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), ⟩, ⟨(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦𝑏 ↦ (𝑔 ∈ ((2nd𝑥)𝑦), 𝑓 ∈ (𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑟)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑠)(2nd𝑦))(2nd𝑓))⟩))⟩})
781, 77wceq 1533 1 wff ×c = (𝑟 ∈ V, 𝑠 ∈ V ↦ ((Base‘𝑟) × (Base‘𝑠)) / 𝑏(𝑢𝑏, 𝑣𝑏 ↦ (((1st𝑢)(Hom ‘𝑟)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑠)(2nd𝑣)))) / {⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), ⟩, ⟨(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦𝑏 ↦ (𝑔 ∈ ((2nd𝑥)𝑦), 𝑓 ∈ (𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑟)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑠)(2nd𝑦))(2nd𝑓))⟩))⟩})
Colors of variables: wff setvar class
This definition is referenced by:  fnxpc  18170  xpcval  18171
  Copyright terms: Public domain W3C validator