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

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