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