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

Definition df-xpc 15298
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 15294 . 2  class  X.c
2 vr . . 3  setvar  r
3 vs . . 3  setvar  s
4 cvv 3113 . . 3  class  _V
5 vb . . . 4  setvar  b
62cv 1378 . . . . . 6  class  r
7 cbs 14489 . . . . . 6  class  Base
86, 7cfv 5587 . . . . 5  class  ( Base `  r )
93cv 1378 . . . . . 6  class  s
109, 7cfv 5587 . . . . 5  class  ( Base `  s )
118, 10cxp 4997 . . . 4  class  ( (
Base `  r )  X.  ( Base `  s
) )
12 vh . . . . 5  setvar  h
13 vu . . . . . 6  setvar  u
14 vv . . . . . 6  setvar  v
155cv 1378 . . . . . 6  class  b
1613cv 1378 . . . . . . . . 9  class  u
17 c1st 6782 . . . . . . . . 9  class  1st
1816, 17cfv 5587 . . . . . . . 8  class  ( 1st `  u )
1914cv 1378 . . . . . . . . 9  class  v
2019, 17cfv 5587 . . . . . . . 8  class  ( 1st `  v )
21 chom 14565 . . . . . . . . 9  class  Hom
226, 21cfv 5587 . . . . . . . 8  class  ( Hom  `  r )
2318, 20, 22co 6283 . . . . . . 7  class  ( ( 1st `  u ) ( Hom  `  r
) ( 1st `  v
) )
24 c2nd 6783 . . . . . . . . 9  class  2nd
2516, 24cfv 5587 . . . . . . . 8  class  ( 2nd `  u )
2619, 24cfv 5587 . . . . . . . 8  class  ( 2nd `  v )
279, 21cfv 5587 . . . . . . . 8  class  ( Hom  `  s )
2825, 26, 27co 6283 . . . . . . 7  class  ( ( 2nd `  u ) ( Hom  `  s
) ( 2nd `  v
) )
2923, 28cxp 4997 . . . . . 6  class  ( ( ( 1st `  u
) ( Hom  `  r
) ( 1st `  v
) )  X.  (
( 2nd `  u
) ( Hom  `  s
) ( 2nd `  v
) ) )
3013, 14, 15, 15, 29cmpt2 6285 . . . . 5  class  ( u  e.  b ,  v  e.  b  |->  ( ( ( 1st `  u
) ( Hom  `  r
) ( 1st `  v
) )  X.  (
( 2nd `  u
) ( Hom  `  s
) ( 2nd `  v
) ) ) )
31 cnx 14486 . . . . . . . 8  class  ndx
3231, 7cfv 5587 . . . . . . 7  class  ( Base `  ndx )
3332, 15cop 4033 . . . . . 6  class  <. ( Base `  ndx ) ,  b >.
3431, 21cfv 5587 . . . . . . 7  class  ( Hom  `  ndx )
3512cv 1378 . . . . . . 7  class  h
3634, 35cop 4033 . . . . . 6  class  <. ( Hom  `  ndx ) ,  h >.
37 cco 14566 . . . . . . . 8  class comp
3831, 37cfv 5587 . . . . . . 7  class  (comp `  ndx )
39 vx . . . . . . . 8  setvar  x
40 vy . . . . . . . 8  setvar  y
4115, 15cxp 4997 . . . . . . . 8  class  ( b  X.  b )
42 vg . . . . . . . . 9  setvar  g
43 vf . . . . . . . . 9  setvar  f
4439cv 1378 . . . . . . . . . . 11  class  x
4544, 24cfv 5587 . . . . . . . . . 10  class  ( 2nd `  x )
4640cv 1378 . . . . . . . . . 10  class  y
4745, 46, 35co 6283 . . . . . . . . 9  class  ( ( 2nd `  x ) h y )
4844, 35cfv 5587 . . . . . . . . 9  class  ( h `
 x )
4942cv 1378 . . . . . . . . . . . 12  class  g
5049, 17cfv 5587 . . . . . . . . . . 11  class  ( 1st `  g )
5143cv 1378 . . . . . . . . . . . 12  class  f
5251, 17cfv 5587 . . . . . . . . . . 11  class  ( 1st `  f )
5344, 17cfv 5587 . . . . . . . . . . . . . 14  class  ( 1st `  x )
5453, 17cfv 5587 . . . . . . . . . . . . 13  class  ( 1st `  ( 1st `  x
) )
5545, 17cfv 5587 . . . . . . . . . . . . 13  class  ( 1st `  ( 2nd `  x
) )
5654, 55cop 4033 . . . . . . . . . . . 12  class  <. ( 1st `  ( 1st `  x
) ) ,  ( 1st `  ( 2nd `  x ) ) >.
5746, 17cfv 5587 . . . . . . . . . . . 12  class  ( 1st `  y )
586, 37cfv 5587 . . . . . . . . . . . 12  class  (comp `  r )
5956, 57, 58co 6283 . . . . . . . . . . 11  class  ( <.
( 1st `  ( 1st `  x ) ) ,  ( 1st `  ( 2nd `  x ) )
>. (comp `  r )
( 1st `  y
) )
6050, 52, 59co 6283 . . . . . . . . . 10  class  ( ( 1st `  g ) ( <. ( 1st `  ( 1st `  x ) ) ,  ( 1st `  ( 2nd `  x ) )
>. (comp `  r )
( 1st `  y
) ) ( 1st `  f ) )
6149, 24cfv 5587 . . . . . . . . . . 11  class  ( 2nd `  g )
6251, 24cfv 5587 . . . . . . . . . . 11  class  ( 2nd `  f )
6353, 24cfv 5587 . . . . . . . . . . . . 13  class  ( 2nd `  ( 1st `  x
) )
6445, 24cfv 5587 . . . . . . . . . . . . 13  class  ( 2nd `  ( 2nd `  x
) )
6563, 64cop 4033 . . . . . . . . . . . 12  class  <. ( 2nd `  ( 1st `  x
) ) ,  ( 2nd `  ( 2nd `  x ) ) >.
6646, 24cfv 5587 . . . . . . . . . . . 12  class  ( 2nd `  y )
679, 37cfv 5587 . . . . . . . . . . . 12  class  (comp `  s )
6865, 66, 67co 6283 . . . . . . . . . . 11  class  ( <.
( 2nd `  ( 1st `  x ) ) ,  ( 2nd `  ( 2nd `  x ) )
>. (comp `  s )
( 2nd `  y
) )
6961, 62, 68co 6283 . . . . . . . . . 10  class  ( ( 2nd `  g ) ( <. ( 2nd `  ( 1st `  x ) ) ,  ( 2nd `  ( 2nd `  x ) )
>. (comp `  s )
( 2nd `  y
) ) ( 2nd `  f ) )
7060, 69cop 4033 . . . . . . . . 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 6285 . . . . . . . 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 6285 . . . . . . 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 4033 . . . . . 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 4031 . . . . 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 3435 . . . 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 3435 . . 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 6285 . 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 1379 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  15302  xpcval  15303
  Copyright terms: Public domain W3C validator