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

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