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