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

Definition df-xpc 15104
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  |-  X.c  =  ( r  e.  _V , 
s  e.  _V  |->  [_ ( ( Base `  r
)  X.  ( Base `  s ) )  / 
b ]_ [_ ( u  e.  b ,  v  e.  b  |->  ( ( ( 1st `  u
) ( Hom  `  r
) ( 1st `  v
) )  X.  (
( 2nd `  u
) ( Hom  `  s
) ( 2nd `  v
) ) ) )  /  h ]_ { <. ( Base `  ndx ) ,  b >. , 
<. ( Hom  `  ndx ) ,  h >. , 
<. (comp `  ndx ) ,  ( x  e.  ( b  X.  b ) ,  y  e.  b 
|->  ( g  e.  ( ( 2nd `  x
) h y ) ,  f  e.  ( h `  x ) 
|->  <. ( ( 1st `  g ) ( <.
( 1st `  ( 1st `  x ) ) ,  ( 1st `  ( 2nd `  x ) )
>. (comp `  r )
( 1st `  y
) ) ( 1st `  f ) ) ,  ( ( 2nd `  g
) ( <. ( 2nd `  ( 1st `  x
) ) ,  ( 2nd `  ( 2nd `  x ) ) >.
(comp `  s )
( 2nd `  y
) ) ( 2nd `  f ) ) >.
) ) >. } )
Distinct variable group:    f, b, g, h, r, s, u, v, x, y

Detailed syntax breakdown of Definition df-xpc
StepHypRef Expression
1 cxpc 15100 . 2  class  X.c
2 vr . . 3  setvar  r
3 vs . . 3  setvar  s
4 cvv 3078 . . 3  class  _V
5 vb . . . 4  setvar  b
62cv 1369 . . . . . 6  class  r
7 cbs 14295 . . . . . 6  class  Base
86, 7cfv 5529 . . . . 5  class  ( Base `  r )
93cv 1369 . . . . . 6  class  s
109, 7cfv 5529 . . . . 5  class  ( Base `  s )
118, 10cxp 4949 . . . 4  class  ( (
Base `  r )  X.  ( Base `  s
) )
12 vh . . . . 5  setvar  h
13 vu . . . . . 6  setvar  u
14 vv . . . . . 6  setvar  v
155cv 1369 . . . . . 6  class  b
1613cv 1369 . . . . . . . . 9  class  u
17 c1st 6688 . . . . . . . . 9  class  1st
1816, 17cfv 5529 . . . . . . . 8  class  ( 1st `  u )
1914cv 1369 . . . . . . . . 9  class  v
2019, 17cfv 5529 . . . . . . . 8  class  ( 1st `  v )
21 chom 14371 . . . . . . . . 9  class  Hom
226, 21cfv 5529 . . . . . . . 8  class  ( Hom  `  r )
2318, 20, 22co 6203 . . . . . . 7  class  ( ( 1st `  u ) ( Hom  `  r
) ( 1st `  v
) )
24 c2nd 6689 . . . . . . . . 9  class  2nd
2516, 24cfv 5529 . . . . . . . 8  class  ( 2nd `  u )
2619, 24cfv 5529 . . . . . . . 8  class  ( 2nd `  v )
279, 21cfv 5529 . . . . . . . 8  class  ( Hom  `  s )
2825, 26, 27co 6203 . . . . . . 7  class  ( ( 2nd `  u ) ( Hom  `  s
) ( 2nd `  v
) )
2923, 28cxp 4949 . . . . . 6  class  ( ( ( 1st `  u
) ( Hom  `  r
) ( 1st `  v
) )  X.  (
( 2nd `  u
) ( Hom  `  s
) ( 2nd `  v
) ) )
3013, 14, 15, 15, 29cmpt2 6205 . . . . 5  class  ( u  e.  b ,  v  e.  b  |->  ( ( ( 1st `  u
) ( Hom  `  r
) ( 1st `  v
) )  X.  (
( 2nd `  u
) ( Hom  `  s
) ( 2nd `  v
) ) ) )
31 cnx 14292 . . . . . . . 8  class  ndx
3231, 7cfv 5529 . . . . . . 7  class  ( Base `  ndx )
3332, 15cop 3994 . . . . . 6  class  <. ( Base `  ndx ) ,  b >.
3431, 21cfv 5529 . . . . . . 7  class  ( Hom  `  ndx )
3512cv 1369 . . . . . . 7  class  h
3634, 35cop 3994 . . . . . 6  class  <. ( Hom  `  ndx ) ,  h >.
37 cco 14372 . . . . . . . 8  class comp
3831, 37cfv 5529 . . . . . . 7  class  (comp `  ndx )
39 vx . . . . . . . 8  setvar  x
40 vy . . . . . . . 8  setvar  y
4115, 15cxp 4949 . . . . . . . 8  class  ( b  X.  b )
42 vg . . . . . . . . 9  setvar  g
43 vf . . . . . . . . 9  setvar  f
4439cv 1369 . . . . . . . . . . 11  class  x
4544, 24cfv 5529 . . . . . . . . . 10  class  ( 2nd `  x )
4640cv 1369 . . . . . . . . . 10  class  y
4745, 46, 35co 6203 . . . . . . . . 9  class  ( ( 2nd `  x ) h y )
4844, 35cfv 5529 . . . . . . . . 9  class  ( h `
 x )
4942cv 1369 . . . . . . . . . . . 12  class  g
5049, 17cfv 5529 . . . . . . . . . . 11  class  ( 1st `  g )
5143cv 1369 . . . . . . . . . . . 12  class  f
5251, 17cfv 5529 . . . . . . . . . . 11  class  ( 1st `  f )
5344, 17cfv 5529 . . . . . . . . . . . . . 14  class  ( 1st `  x )
5453, 17cfv 5529 . . . . . . . . . . . . 13  class  ( 1st `  ( 1st `  x
) )
5545, 17cfv 5529 . . . . . . . . . . . . 13  class  ( 1st `  ( 2nd `  x
) )
5654, 55cop 3994 . . . . . . . . . . . 12  class  <. ( 1st `  ( 1st `  x
) ) ,  ( 1st `  ( 2nd `  x ) ) >.
5746, 17cfv 5529 . . . . . . . . . . . 12  class  ( 1st `  y )
586, 37cfv 5529 . . . . . . . . . . . 12  class  (comp `  r )
5956, 57, 58co 6203 . . . . . . . . . . 11  class  ( <.
( 1st `  ( 1st `  x ) ) ,  ( 1st `  ( 2nd `  x ) )
>. (comp `  r )
( 1st `  y
) )
6050, 52, 59co 6203 . . . . . . . . . 10  class  ( ( 1st `  g ) ( <. ( 1st `  ( 1st `  x ) ) ,  ( 1st `  ( 2nd `  x ) )
>. (comp `  r )
( 1st `  y
) ) ( 1st `  f ) )
6149, 24cfv 5529 . . . . . . . . . . 11  class  ( 2nd `  g )
6251, 24cfv 5529 . . . . . . . . . . 11  class  ( 2nd `  f )
6353, 24cfv 5529 . . . . . . . . . . . . 13  class  ( 2nd `  ( 1st `  x
) )
6445, 24cfv 5529 . . . . . . . . . . . . 13  class  ( 2nd `  ( 2nd `  x
) )
6563, 64cop 3994 . . . . . . . . . . . 12  class  <. ( 2nd `  ( 1st `  x
) ) ,  ( 2nd `  ( 2nd `  x ) ) >.
6646, 24cfv 5529 . . . . . . . . . . . 12  class  ( 2nd `  y )
679, 37cfv 5529 . . . . . . . . . . . 12  class  (comp `  s )
6865, 66, 67co 6203 . . . . . . . . . . 11  class  ( <.
( 2nd `  ( 1st `  x ) ) ,  ( 2nd `  ( 2nd `  x ) )
>. (comp `  s )
( 2nd `  y
) )
6961, 62, 68co 6203 . . . . . . . . . 10  class  ( ( 2nd `  g ) ( <. ( 2nd `  ( 1st `  x ) ) ,  ( 2nd `  ( 2nd `  x ) )
>. (comp `  s )
( 2nd `  y
) ) ( 2nd `  f ) )
7060, 69cop 3994 . . . . . . . . 9  class  <. (
( 1st `  g
) ( <. ( 1st `  ( 1st `  x
) ) ,  ( 1st `  ( 2nd `  x ) ) >.
(comp `  r )
( 1st `  y
) ) ( 1st `  f ) ) ,  ( ( 2nd `  g
) ( <. ( 2nd `  ( 1st `  x
) ) ,  ( 2nd `  ( 2nd `  x ) ) >.
(comp `  s )
( 2nd `  y
) ) ( 2nd `  f ) ) >.
7142, 43, 47, 48, 70cmpt2 6205 . . . . . . . 8  class  ( g  e.  ( ( 2nd `  x ) h y ) ,  f  e.  ( h `  x
)  |->  <. ( ( 1st `  g ) ( <.
( 1st `  ( 1st `  x ) ) ,  ( 1st `  ( 2nd `  x ) )
>. (comp `  r )
( 1st `  y
) ) ( 1st `  f ) ) ,  ( ( 2nd `  g
) ( <. ( 2nd `  ( 1st `  x
) ) ,  ( 2nd `  ( 2nd `  x ) ) >.
(comp `  s )
( 2nd `  y
) ) ( 2nd `  f ) ) >.
)
7239, 40, 41, 15, 71cmpt2 6205 . . . . . . 7  class  ( x  e.  ( b  X.  b ) ,  y  e.  b  |->  ( g  e.  ( ( 2nd `  x ) h y ) ,  f  e.  ( h `  x
)  |->  <. ( ( 1st `  g ) ( <.
( 1st `  ( 1st `  x ) ) ,  ( 1st `  ( 2nd `  x ) )
>. (comp `  r )
( 1st `  y
) ) ( 1st `  f ) ) ,  ( ( 2nd `  g
) ( <. ( 2nd `  ( 1st `  x
) ) ,  ( 2nd `  ( 2nd `  x ) ) >.
(comp `  s )
( 2nd `  y
) ) ( 2nd `  f ) ) >.
) )
7338, 72cop 3994 . . . . . 6  class  <. (comp ` 
ndx ) ,  ( x  e.  ( b  X.  b ) ,  y  e.  b  |->  ( g  e.  ( ( 2nd `  x ) h y ) ,  f  e.  ( h `
 x )  |->  <.
( ( 1st `  g
) ( <. ( 1st `  ( 1st `  x
) ) ,  ( 1st `  ( 2nd `  x ) ) >.
(comp `  r )
( 1st `  y
) ) ( 1st `  f ) ) ,  ( ( 2nd `  g
) ( <. ( 2nd `  ( 1st `  x
) ) ,  ( 2nd `  ( 2nd `  x ) ) >.
(comp `  s )
( 2nd `  y
) ) ( 2nd `  f ) ) >.
) ) >.
7433, 36, 73ctp 3992 . . . . 5  class  { <. (
Base `  ndx ) ,  b >. ,  <. ( Hom  `  ndx ) ,  h >. ,  <. (comp ` 
ndx ) ,  ( x  e.  ( b  X.  b ) ,  y  e.  b  |->  ( g  e.  ( ( 2nd `  x ) h y ) ,  f  e.  ( h `
 x )  |->  <.
( ( 1st `  g
) ( <. ( 1st `  ( 1st `  x
) ) ,  ( 1st `  ( 2nd `  x ) ) >.
(comp `  r )
( 1st `  y
) ) ( 1st `  f ) ) ,  ( ( 2nd `  g
) ( <. ( 2nd `  ( 1st `  x
) ) ,  ( 2nd `  ( 2nd `  x ) ) >.
(comp `  s )
( 2nd `  y
) ) ( 2nd `  f ) ) >.
) ) >. }
7512, 30, 74csb 3398 . . . 4  class  [_ (
u  e.  b ,  v  e.  b  |->  ( ( ( 1st `  u
) ( Hom  `  r
) ( 1st `  v
) )  X.  (
( 2nd `  u
) ( Hom  `  s
) ( 2nd `  v
) ) ) )  /  h ]_ { <. ( Base `  ndx ) ,  b >. , 
<. ( Hom  `  ndx ) ,  h >. , 
<. (comp `  ndx ) ,  ( x  e.  ( b  X.  b ) ,  y  e.  b 
|->  ( g  e.  ( ( 2nd `  x
) h y ) ,  f  e.  ( h `  x ) 
|->  <. ( ( 1st `  g ) ( <.
( 1st `  ( 1st `  x ) ) ,  ( 1st `  ( 2nd `  x ) )
>. (comp `  r )
( 1st `  y
) ) ( 1st `  f ) ) ,  ( ( 2nd `  g
) ( <. ( 2nd `  ( 1st `  x
) ) ,  ( 2nd `  ( 2nd `  x ) ) >.
(comp `  s )
( 2nd `  y
) ) ( 2nd `  f ) ) >.
) ) >. }
765, 11, 75csb 3398 . . 3  class  [_ (
( Base `  r )  X.  ( Base `  s
) )  /  b ]_ [_ ( u  e.  b ,  v  e.  b  |->  ( ( ( 1st `  u ) ( Hom  `  r
) ( 1st `  v
) )  X.  (
( 2nd `  u
) ( Hom  `  s
) ( 2nd `  v
) ) ) )  /  h ]_ { <. ( Base `  ndx ) ,  b >. , 
<. ( Hom  `  ndx ) ,  h >. , 
<. (comp `  ndx ) ,  ( x  e.  ( b  X.  b ) ,  y  e.  b 
|->  ( g  e.  ( ( 2nd `  x
) h y ) ,  f  e.  ( h `  x ) 
|->  <. ( ( 1st `  g ) ( <.
( 1st `  ( 1st `  x ) ) ,  ( 1st `  ( 2nd `  x ) )
>. (comp `  r )
( 1st `  y
) ) ( 1st `  f ) ) ,  ( ( 2nd `  g
) ( <. ( 2nd `  ( 1st `  x
) ) ,  ( 2nd `  ( 2nd `  x ) ) >.
(comp `  s )
( 2nd `  y
) ) ( 2nd `  f ) ) >.
) ) >. }
772, 3, 4, 4, 76cmpt2 6205 . 2  class  ( r  e.  _V ,  s  e.  _V  |->  [_ (
( Base `  r )  X.  ( Base `  s
) )  /  b ]_ [_ ( u  e.  b ,  v  e.  b  |->  ( ( ( 1st `  u ) ( Hom  `  r
) ( 1st `  v
) )  X.  (
( 2nd `  u
) ( Hom  `  s
) ( 2nd `  v
) ) ) )  /  h ]_ { <. ( Base `  ndx ) ,  b >. , 
<. ( Hom  `  ndx ) ,  h >. , 
<. (comp `  ndx ) ,  ( x  e.  ( b  X.  b ) ,  y  e.  b 
|->  ( g  e.  ( ( 2nd `  x
) h y ) ,  f  e.  ( h `  x ) 
|->  <. ( ( 1st `  g ) ( <.
( 1st `  ( 1st `  x ) ) ,  ( 1st `  ( 2nd `  x ) )
>. (comp `  r )
( 1st `  y
) ) ( 1st `  f ) ) ,  ( ( 2nd `  g
) ( <. ( 2nd `  ( 1st `  x
) ) ,  ( 2nd `  ( 2nd `  x ) ) >.
(comp `  s )
( 2nd `  y
) ) ( 2nd `  f ) ) >.
) ) >. } )
781, 77wceq 1370 1  wff  X.c  =  ( r  e.  _V , 
s  e.  _V  |->  [_ ( ( Base `  r
)  X.  ( Base `  s ) )  / 
b ]_ [_ ( u  e.  b ,  v  e.  b  |->  ( ( ( 1st `  u
) ( Hom  `  r
) ( 1st `  v
) )  X.  (
( 2nd `  u
) ( Hom  `  s
) ( 2nd `  v
) ) ) )  /  h ]_ { <. ( Base `  ndx ) ,  b >. , 
<. ( Hom  `  ndx ) ,  h >. , 
<. (comp `  ndx ) ,  ( x  e.  ( b  X.  b ) ,  y  e.  b 
|->  ( g  e.  ( ( 2nd `  x
) h y ) ,  f  e.  ( h `  x ) 
|->  <. ( ( 1st `  g ) ( <.
( 1st `  ( 1st `  x ) ) ,  ( 1st `  ( 2nd `  x ) )
>. (comp `  r )
( 1st `  y
) ) ( 1st `  f ) ) ,  ( ( 2nd `  g
) ( <. ( 2nd `  ( 1st `  x
) ) ,  ( 2nd `  ( 2nd `  x ) ) >.
(comp `  s )
( 2nd `  y
) ) ( 2nd `  f ) ) >.
) ) >. } )
Colors of variables: wff setvar class
This definition is referenced by:  fnxpc  15108  xpcval  15109
  Copyright terms: Public domain W3C validator