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

Definition df-xpc 13946
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 13942 . 2  class  X.c
2 vr . . 3  set  r
3 vs . . 3  set  s
4 cvv 2788 . . 3  class  _V
5 vb . . . 4  set  b
62cv 1622 . . . . . 6  class  r
7 cbs 13148 . . . . . 6  class  Base
86, 7cfv 5255 . . . . 5  class  ( Base `  r )
93cv 1622 . . . . . 6  class  s
109, 7cfv 5255 . . . . 5  class  ( Base `  s )
118, 10cxp 4687 . . . 4  class  ( (
Base `  r )  X.  ( Base `  s
) )
12 vh . . . . 5  set  h
13 vu . . . . . 6  set  u
14 vv . . . . . 6  set  v
155cv 1622 . . . . . 6  class  b
1613cv 1622 . . . . . . . . 9  class  u
17 c1st 6120 . . . . . . . . 9  class  1st
1816, 17cfv 5255 . . . . . . . 8  class  ( 1st `  u )
1914cv 1622 . . . . . . . . 9  class  v
2019, 17cfv 5255 . . . . . . . 8  class  ( 1st `  v )
21 chom 13219 . . . . . . . . 9  class  Hom
226, 21cfv 5255 . . . . . . . 8  class  (  Hom  `  r )
2318, 20, 22co 5858 . . . . . . 7  class  ( ( 1st `  u ) (  Hom  `  r
) ( 1st `  v
) )
24 c2nd 6121 . . . . . . . . 9  class  2nd
2516, 24cfv 5255 . . . . . . . 8  class  ( 2nd `  u )
2619, 24cfv 5255 . . . . . . . 8  class  ( 2nd `  v )
279, 21cfv 5255 . . . . . . . 8  class  (  Hom  `  s )
2825, 26, 27co 5858 . . . . . . 7  class  ( ( 2nd `  u ) (  Hom  `  s
) ( 2nd `  v
) )
2923, 28cxp 4687 . . . . . 6  class  ( ( ( 1st `  u
) (  Hom  `  r
) ( 1st `  v
) )  X.  (
( 2nd `  u
) (  Hom  `  s
) ( 2nd `  v
) ) )
3013, 14, 15, 15, 29cmpt2 5860 . . . . 5  class  ( u  e.  b ,  v  e.  b  |->  ( ( ( 1st `  u
) (  Hom  `  r
) ( 1st `  v
) )  X.  (
( 2nd `  u
) (  Hom  `  s
) ( 2nd `  v
) ) ) )
31 cnx 13145 . . . . . . . 8  class  ndx
3231, 7cfv 5255 . . . . . . 7  class  ( Base `  ndx )
3332, 15cop 3643 . . . . . 6  class  <. ( Base `  ndx ) ,  b >.
3431, 21cfv 5255 . . . . . . 7  class  (  Hom  `  ndx )
3512cv 1622 . . . . . . 7  class  h
3634, 35cop 3643 . . . . . 6  class  <. (  Hom  `  ndx ) ,  h >.
37 cco 13220 . . . . . . . 8  class comp
3831, 37cfv 5255 . . . . . . 7  class  (comp `  ndx )
39 vx . . . . . . . 8  set  x
40 vy . . . . . . . 8  set  y
4115, 15cxp 4687 . . . . . . . 8  class  ( b  X.  b )
42 vg . . . . . . . . 9  set  g
43 vf . . . . . . . . 9  set  f
4439cv 1622 . . . . . . . . . . 11  class  x
4544, 24cfv 5255 . . . . . . . . . 10  class  ( 2nd `  x )
4640cv 1622 . . . . . . . . . 10  class  y
4745, 46, 35co 5858 . . . . . . . . 9  class  ( ( 2nd `  x ) h y )
4844, 35cfv 5255 . . . . . . . . 9  class  ( h `
 x )
4942cv 1622 . . . . . . . . . . . 12  class  g
5049, 17cfv 5255 . . . . . . . . . . 11  class  ( 1st `  g )
5143cv 1622 . . . . . . . . . . . 12  class  f
5251, 17cfv 5255 . . . . . . . . . . 11  class  ( 1st `  f )
5344, 17cfv 5255 . . . . . . . . . . . . . 14  class  ( 1st `  x )
5453, 17cfv 5255 . . . . . . . . . . . . 13  class  ( 1st `  ( 1st `  x
) )
5545, 17cfv 5255 . . . . . . . . . . . . 13  class  ( 1st `  ( 2nd `  x
) )
5654, 55cop 3643 . . . . . . . . . . . 12  class  <. ( 1st `  ( 1st `  x
) ) ,  ( 1st `  ( 2nd `  x ) ) >.
5746, 17cfv 5255 . . . . . . . . . . . 12  class  ( 1st `  y )
586, 37cfv 5255 . . . . . . . . . . . 12  class  (comp `  r )
5956, 57, 58co 5858 . . . . . . . . . . 11  class  ( <.
( 1st `  ( 1st `  x ) ) ,  ( 1st `  ( 2nd `  x ) )
>. (comp `  r )
( 1st `  y
) )
6050, 52, 59co 5858 . . . . . . . . . 10  class  ( ( 1st `  g ) ( <. ( 1st `  ( 1st `  x ) ) ,  ( 1st `  ( 2nd `  x ) )
>. (comp `  r )
( 1st `  y
) ) ( 1st `  f ) )
6149, 24cfv 5255 . . . . . . . . . . 11  class  ( 2nd `  g )
6251, 24cfv 5255 . . . . . . . . . . 11  class  ( 2nd `  f )
6353, 24cfv 5255 . . . . . . . . . . . . 13  class  ( 2nd `  ( 1st `  x
) )
6445, 24cfv 5255 . . . . . . . . . . . . 13  class  ( 2nd `  ( 2nd `  x
) )
6563, 64cop 3643 . . . . . . . . . . . 12  class  <. ( 2nd `  ( 1st `  x
) ) ,  ( 2nd `  ( 2nd `  x ) ) >.
6646, 24cfv 5255 . . . . . . . . . . . 12  class  ( 2nd `  y )
679, 37cfv 5255 . . . . . . . . . . . 12  class  (comp `  s )
6865, 66, 67co 5858 . . . . . . . . . . 11  class  ( <.
( 2nd `  ( 1st `  x ) ) ,  ( 2nd `  ( 2nd `  x ) )
>. (comp `  s )
( 2nd `  y
) )
6961, 62, 68co 5858 . . . . . . . . . 10  class  ( ( 2nd `  g ) ( <. ( 2nd `  ( 1st `  x ) ) ,  ( 2nd `  ( 2nd `  x ) )
>. (comp `  s )
( 2nd `  y
) ) ( 2nd `  f ) )
7060, 69cop 3643 . . . . . . . . 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 5860 . . . . . . . 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 5860 . . . . . . 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 3643 . . . . . 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 3642 . . . . 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 3081 . . . 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 3081 . . 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 5860 . 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 1623 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  13950  xpcval  13951
  Copyright terms: Public domain W3C validator