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