MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fnxpc Structured version   Visualization version   Unicode version

Theorem fnxpc 16061
Description: The binary product of categories is a two-argument function. (Contributed by Mario Carneiro, 10-Jan-2017.)
Assertion
Ref Expression
fnxpc  |-  X.c  Fn  ( _V  X.  _V )

Proof of Theorem fnxpc
Dummy variables  f 
b  g  h  r  s  u  v  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-xpc 16057 . 2  |-  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 ) ) >.
) ) >. } )
2 tpex 6590 . . . 4  |-  { <. (
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 ) ) >.
) ) >. }  e.  _V
32csbex 4538 . . 3  |-  [_ (
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 ) ) >.
) ) >. }  e.  _V
43csbex 4538 . 2  |-  [_ (
( 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 ) ) >.
) ) >. }  e.  _V
51, 4fnmpt2i 6862 1  |-  X.c  Fn  ( _V  X.  _V )
Colors of variables: wff setvar class
Syntax hints:   _Vcvv 3045   [_csb 3363   {ctp 3972   <.cop 3974    X. cxp 4832    Fn wfn 5577   ` cfv 5582  (class class class)co 6290    |-> cmpt2 6292   1stc1st 6791   2ndc2nd 6792   ndxcnx 15118   Basecbs 15121   Hom chom 15201  compcco 15202    X.c cxpc 16053
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-fal 1450  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-fv 5590  df-oprab 6294  df-mpt2 6295  df-1st 6793  df-2nd 6794  df-xpc 16057
This theorem is referenced by:  xpcbas  16063  xpchomfval  16064  xpccofval  16067
  Copyright terms: Public domain W3C validator