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

Definition df-xpc 14228
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 14224 . 2  class  X.c
2 vr . . 3  set  r
3 vs . . 3  set  s
4 cvv 2920 . . 3  class  _V
5 vb . . . 4  set  b
62cv 1648 . . . . . 6  class  r
7 cbs 13428 . . . . . 6  class  Base
86, 7cfv 5417 . . . . 5  class  ( Base `  r )
93cv 1648 . . . . . 6  class  s
109, 7cfv 5417 . . . . 5  class  ( Base `  s )
118, 10cxp 4839 . . . 4  class  ( (
Base `  r )  X.  ( Base `  s
) )
12 vh . . . . 5  set  h
13 vu . . . . . 6  set  u
14 vv . . . . . 6  set  v
155cv 1648 . . . . . 6  class  b
1613cv 1648 . . . . . . . . 9  class  u
17 c1st 6310 . . . . . . . . 9  class  1st
1816, 17cfv 5417 . . . . . . . 8  class  ( 1st `  u )
1914cv 1648 . . . . . . . . 9  class  v
2019, 17cfv 5417 . . . . . . . 8  class  ( 1st `  v )
21 chom 13499 . . . . . . . . 9  class  Hom
226, 21cfv 5417 . . . . . . . 8  class  (  Hom  `  r )
2318, 20, 22co 6044 . . . . . . 7  class  ( ( 1st `  u ) (  Hom  `  r
) ( 1st `  v
) )
24 c2nd 6311 . . . . . . . . 9  class  2nd
2516, 24cfv 5417 . . . . . . . 8  class  ( 2nd `  u )
2619, 24cfv 5417 . . . . . . . 8  class  ( 2nd `  v )
279, 21cfv 5417 . . . . . . . 8  class  (  Hom  `  s )
2825, 26, 27co 6044 . . . . . . 7  class  ( ( 2nd `  u ) (  Hom  `  s
) ( 2nd `  v
) )
2923, 28cxp 4839 . . . . . 6  class  ( ( ( 1st `  u
) (  Hom  `  r
) ( 1st `  v
) )  X.  (
( 2nd `  u
) (  Hom  `  s
) ( 2nd `  v
) ) )
3013, 14, 15, 15, 29cmpt2 6046 . . . . 5  class  ( u  e.  b ,  v  e.  b  |->  ( ( ( 1st `  u
) (  Hom  `  r
) ( 1st `  v
) )  X.  (
( 2nd `  u
) (  Hom  `  s
) ( 2nd `  v
) ) ) )
31 cnx 13425 . . . . . . . 8  class  ndx
3231, 7cfv 5417 . . . . . . 7  class  ( Base `  ndx )
3332, 15cop 3781 . . . . . 6  class  <. ( Base `  ndx ) ,  b >.
3431, 21cfv 5417 . . . . . . 7  class  (  Hom  `  ndx )
3512cv 1648 . . . . . . 7  class  h
3634, 35cop 3781 . . . . . 6  class  <. (  Hom  `  ndx ) ,  h >.
37 cco 13500 . . . . . . . 8  class comp
3831, 37cfv 5417 . . . . . . 7  class  (comp `  ndx )
39 vx . . . . . . . 8  set  x
40 vy . . . . . . . 8  set  y
4115, 15cxp 4839 . . . . . . . 8  class  ( b  X.  b )
42 vg . . . . . . . . 9  set  g
43 vf . . . . . . . . 9  set  f
4439cv 1648 . . . . . . . . . . 11  class  x
4544, 24cfv 5417 . . . . . . . . . 10  class  ( 2nd `  x )
4640cv 1648 . . . . . . . . . 10  class  y
4745, 46, 35co 6044 . . . . . . . . 9  class  ( ( 2nd `  x ) h y )
4844, 35cfv 5417 . . . . . . . . 9  class  ( h `
 x )
4942cv 1648 . . . . . . . . . . . 12  class  g
5049, 17cfv 5417 . . . . . . . . . . 11  class  ( 1st `  g )
5143cv 1648 . . . . . . . . . . . 12  class  f
5251, 17cfv 5417 . . . . . . . . . . 11  class  ( 1st `  f )
5344, 17cfv 5417 . . . . . . . . . . . . . 14  class  ( 1st `  x )
5453, 17cfv 5417 . . . . . . . . . . . . 13  class  ( 1st `  ( 1st `  x
) )
5545, 17cfv 5417 . . . . . . . . . . . . 13  class  ( 1st `  ( 2nd `  x
) )
5654, 55cop 3781 . . . . . . . . . . . 12  class  <. ( 1st `  ( 1st `  x
) ) ,  ( 1st `  ( 2nd `  x ) ) >.
5746, 17cfv 5417 . . . . . . . . . . . 12  class  ( 1st `  y )
586, 37cfv 5417 . . . . . . . . . . . 12  class  (comp `  r )
5956, 57, 58co 6044 . . . . . . . . . . 11  class  ( <.
( 1st `  ( 1st `  x ) ) ,  ( 1st `  ( 2nd `  x ) )
>. (comp `  r )
( 1st `  y
) )
6050, 52, 59co 6044 . . . . . . . . . 10  class  ( ( 1st `  g ) ( <. ( 1st `  ( 1st `  x ) ) ,  ( 1st `  ( 2nd `  x ) )
>. (comp `  r )
( 1st `  y
) ) ( 1st `  f ) )
6149, 24cfv 5417 . . . . . . . . . . 11  class  ( 2nd `  g )
6251, 24cfv 5417 . . . . . . . . . . 11  class  ( 2nd `  f )
6353, 24cfv 5417 . . . . . . . . . . . . 13  class  ( 2nd `  ( 1st `  x
) )
6445, 24cfv 5417 . . . . . . . . . . . . 13  class  ( 2nd `  ( 2nd `  x
) )
6563, 64cop 3781 . . . . . . . . . . . 12  class  <. ( 2nd `  ( 1st `  x
) ) ,  ( 2nd `  ( 2nd `  x ) ) >.
6646, 24cfv 5417 . . . . . . . . . . . 12  class  ( 2nd `  y )
679, 37cfv 5417 . . . . . . . . . . . 12  class  (comp `  s )
6865, 66, 67co 6044 . . . . . . . . . . 11  class  ( <.
( 2nd `  ( 1st `  x ) ) ,  ( 2nd `  ( 2nd `  x ) )
>. (comp `  s )
( 2nd `  y
) )
6961, 62, 68co 6044 . . . . . . . . . 10  class  ( ( 2nd `  g ) ( <. ( 2nd `  ( 1st `  x ) ) ,  ( 2nd `  ( 2nd `  x ) )
>. (comp `  s )
( 2nd `  y
) ) ( 2nd `  f ) )
7060, 69cop 3781 . . . . . . . . 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 6046 . . . . . . . 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 6046 . . . . . . 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 3781 . . . . . 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 3780 . . . . 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 3215 . . . 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 3215 . . 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 6046 . 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 1649 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 set class
This definition is referenced by:  fnxpc  14232  xpcval  14233
  Copyright terms: Public domain W3C validator