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 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‘𝑠)) / 𝑏(𝑢𝑏, 𝑣𝑏 ↦ (((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 18056 . 2 class ×c
2 vr . . 3 setvar 𝑟
3 vs . . 3 setvar 𝑠
4 cvv 3445 . . 3 class V
5 vb . . . 4 setvar 𝑏
62cv 1540 . . . . . 6 class 𝑟
7 cbs 17083 . . . . . 6 class Base
86, 7cfv 6496 . . . . 5 class (Base‘𝑟)
93cv 1540 . . . . . 6 class 𝑠
109, 7cfv 6496 . . . . 5 class (Base‘𝑠)
118, 10cxp 5631 . . . 4 class ((Base‘𝑟) × (Base‘𝑠))
12 vh . . . . 5 setvar
13 vu . . . . . 6 setvar 𝑢
14 vv . . . . . 6 setvar 𝑣
155cv 1540 . . . . . 6 class 𝑏
1613cv 1540 . . . . . . . . 9 class 𝑢
17 c1st 7919 . . . . . . . . 9 class 1st
1816, 17cfv 6496 . . . . . . . 8 class (1st𝑢)
1914cv 1540 . . . . . . . . 9 class 𝑣
2019, 17cfv 6496 . . . . . . . 8 class (1st𝑣)
21 chom 17144 . . . . . . . . 9 class Hom
226, 21cfv 6496 . . . . . . . 8 class (Hom ‘𝑟)
2318, 20, 22co 7357 . . . . . . 7 class ((1st𝑢)(Hom ‘𝑟)(1st𝑣))
24 c2nd 7920 . . . . . . . . 9 class 2nd
2516, 24cfv 6496 . . . . . . . 8 class (2nd𝑢)
2619, 24cfv 6496 . . . . . . . 8 class (2nd𝑣)
279, 21cfv 6496 . . . . . . . 8 class (Hom ‘𝑠)
2825, 26, 27co 7357 . . . . . . 7 class ((2nd𝑢)(Hom ‘𝑠)(2nd𝑣))
2923, 28cxp 5631 . . . . . 6 class (((1st𝑢)(Hom ‘𝑟)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑠)(2nd𝑣)))
3013, 14, 15, 15, 29cmpo 7359 . . . . 5 class (𝑢𝑏, 𝑣𝑏 ↦ (((1st𝑢)(Hom ‘𝑟)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑠)(2nd𝑣))))
31 cnx 17065 . . . . . . . 8 class ndx
3231, 7cfv 6496 . . . . . . 7 class (Base‘ndx)
3332, 15cop 4592 . . . . . 6 class ⟨(Base‘ndx), 𝑏
3431, 21cfv 6496 . . . . . . 7 class (Hom ‘ndx)
3512cv 1540 . . . . . . 7 class
3634, 35cop 4592 . . . . . 6 class ⟨(Hom ‘ndx),
37 cco 17145 . . . . . . . 8 class comp
3831, 37cfv 6496 . . . . . . 7 class (comp‘ndx)
39 vx . . . . . . . 8 setvar 𝑥
40 vy . . . . . . . 8 setvar 𝑦
4115, 15cxp 5631 . . . . . . . 8 class (𝑏 × 𝑏)
42 vg . . . . . . . . 9 setvar 𝑔
43 vf . . . . . . . . 9 setvar 𝑓
4439cv 1540 . . . . . . . . . . 11 class 𝑥
4544, 24cfv 6496 . . . . . . . . . 10 class (2nd𝑥)
4640cv 1540 . . . . . . . . . 10 class 𝑦
4745, 46, 35co 7357 . . . . . . . . 9 class ((2nd𝑥)𝑦)
4844, 35cfv 6496 . . . . . . . . 9 class (𝑥)
4942cv 1540 . . . . . . . . . . . 12 class 𝑔
5049, 17cfv 6496 . . . . . . . . . . 11 class (1st𝑔)
5143cv 1540 . . . . . . . . . . . 12 class 𝑓
5251, 17cfv 6496 . . . . . . . . . . 11 class (1st𝑓)
5344, 17cfv 6496 . . . . . . . . . . . . . 14 class (1st𝑥)
5453, 17cfv 6496 . . . . . . . . . . . . 13 class (1st ‘(1st𝑥))
5545, 17cfv 6496 . . . . . . . . . . . . 13 class (1st ‘(2nd𝑥))
5654, 55cop 4592 . . . . . . . . . . . 12 class ⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩
5746, 17cfv 6496 . . . . . . . . . . . 12 class (1st𝑦)
586, 37cfv 6496 . . . . . . . . . . . 12 class (comp‘𝑟)
5956, 57, 58co 7357 . . . . . . . . . . 11 class (⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑟)(1st𝑦))
6050, 52, 59co 7357 . . . . . . . . . 10 class ((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑟)(1st𝑦))(1st𝑓))
6149, 24cfv 6496 . . . . . . . . . . 11 class (2nd𝑔)
6251, 24cfv 6496 . . . . . . . . . . 11 class (2nd𝑓)
6353, 24cfv 6496 . . . . . . . . . . . . 13 class (2nd ‘(1st𝑥))
6445, 24cfv 6496 . . . . . . . . . . . . 13 class (2nd ‘(2nd𝑥))
6563, 64cop 4592 . . . . . . . . . . . 12 class ⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩
6646, 24cfv 6496 . . . . . . . . . . . 12 class (2nd𝑦)
679, 37cfv 6496 . . . . . . . . . . . 12 class (comp‘𝑠)
6865, 66, 67co 7357 . . . . . . . . . . 11 class (⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑠)(2nd𝑦))
6961, 62, 68co 7357 . . . . . . . . . 10 class ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑠)(2nd𝑦))(2nd𝑓))
7060, 69cop 4592 . . . . . . . . 9 class ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑟)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑠)(2nd𝑦))(2nd𝑓))⟩
7142, 43, 47, 48, 70cmpo 7359 . . . . . . . 8 class (𝑔 ∈ ((2nd𝑥)𝑦), 𝑓 ∈ (𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑟)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑠)(2nd𝑦))(2nd𝑓))⟩)
7239, 40, 41, 15, 71cmpo 7359 . . . . . . 7 class (𝑥 ∈ (𝑏 × 𝑏), 𝑦𝑏 ↦ (𝑔 ∈ ((2nd𝑥)𝑦), 𝑓 ∈ (𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑟)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑠)(2nd𝑦))(2nd𝑓))⟩))
7338, 72cop 4592 . . . . . 6 class ⟨(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦𝑏 ↦ (𝑔 ∈ ((2nd𝑥)𝑦), 𝑓 ∈ (𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑟)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑠)(2nd𝑦))(2nd𝑓))⟩))⟩
7433, 36, 73ctp 4590 . . . . 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 3855 . . . 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 3855 . . 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 7359 . 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 1541 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  18064  xpcval  18065
  Copyright terms: Public domain W3C validator