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

Definition df-prf 13949
Description: Define the pairing operation for functors (which takes two functors  F : C --> D and  G : C --> E and produces  ( F ⟨,⟩F  G ) : C --> ( D  X.c  E )). (Contributed by Mario Carneiro, 11-Jan-2017.)
Assertion
Ref Expression
df-prf  |- ⟨,⟩F  =  ( f  e. 
_V ,  g  e. 
_V  |->  [_ dom  ( 1st `  f )  /  b ]_ <. ( x  e.  b  |->  <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
) ,  ( x  e.  b ,  y  e.  b  |->  ( h  e.  dom  ( x ( 2nd `  f
) y )  |->  <.
( ( x ( 2nd `  f ) y ) `  h
) ,  ( ( x ( 2nd `  g
) y ) `  h ) >. )
) >. )
Distinct variable group:    f, b, g, h, x, y

Detailed syntax breakdown of Definition df-prf
StepHypRef Expression
1 cprf 13945 . 2  class ⟨,⟩F
2 vf . . 3  set  f
3 vg . . 3  set  g
4 cvv 2788 . . 3  class  _V
5 vb . . . 4  set  b
62cv 1622 . . . . . 6  class  f
7 c1st 6120 . . . . . 6  class  1st
86, 7cfv 5255 . . . . 5  class  ( 1st `  f )
98cdm 4689 . . . 4  class  dom  ( 1st `  f )
10 vx . . . . . 6  set  x
115cv 1622 . . . . . 6  class  b
1210cv 1622 . . . . . . . 8  class  x
1312, 8cfv 5255 . . . . . . 7  class  ( ( 1st `  f ) `
 x )
143cv 1622 . . . . . . . . 9  class  g
1514, 7cfv 5255 . . . . . . . 8  class  ( 1st `  g )
1612, 15cfv 5255 . . . . . . 7  class  ( ( 1st `  g ) `
 x )
1713, 16cop 3643 . . . . . 6  class  <. (
( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >.
1810, 11, 17cmpt 4077 . . . . 5  class  ( x  e.  b  |->  <. (
( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. )
19 vy . . . . . 6  set  y
20 vh . . . . . . 7  set  h
2119cv 1622 . . . . . . . . 9  class  y
22 c2nd 6121 . . . . . . . . . 10  class  2nd
236, 22cfv 5255 . . . . . . . . 9  class  ( 2nd `  f )
2412, 21, 23co 5858 . . . . . . . 8  class  ( x ( 2nd `  f
) y )
2524cdm 4689 . . . . . . 7  class  dom  (
x ( 2nd `  f
) y )
2620cv 1622 . . . . . . . . 9  class  h
2726, 24cfv 5255 . . . . . . . 8  class  ( ( x ( 2nd `  f
) y ) `  h )
2814, 22cfv 5255 . . . . . . . . . 10  class  ( 2nd `  g )
2912, 21, 28co 5858 . . . . . . . . 9  class  ( x ( 2nd `  g
) y )
3026, 29cfv 5255 . . . . . . . 8  class  ( ( x ( 2nd `  g
) y ) `  h )
3127, 30cop 3643 . . . . . . 7  class  <. (
( x ( 2nd `  f ) y ) `
 h ) ,  ( ( x ( 2nd `  g ) y ) `  h
) >.
3220, 25, 31cmpt 4077 . . . . . 6  class  ( h  e.  dom  ( x ( 2nd `  f
) y )  |->  <.
( ( x ( 2nd `  f ) y ) `  h
) ,  ( ( x ( 2nd `  g
) y ) `  h ) >. )
3310, 19, 11, 11, 32cmpt2 5860 . . . . 5  class  ( x  e.  b ,  y  e.  b  |->  ( h  e.  dom  ( x ( 2nd `  f
) y )  |->  <.
( ( x ( 2nd `  f ) y ) `  h
) ,  ( ( x ( 2nd `  g
) y ) `  h ) >. )
)
3418, 33cop 3643 . . . 4  class  <. (
x  e.  b  |->  <.
( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. ) ,  ( x  e.  b ,  y  e.  b  |->  ( h  e.  dom  (
x ( 2nd `  f
) y )  |->  <.
( ( x ( 2nd `  f ) y ) `  h
) ,  ( ( x ( 2nd `  g
) y ) `  h ) >. )
) >.
355, 9, 34csb 3081 . . 3  class  [_ dom  ( 1st `  f )  /  b ]_ <. ( x  e.  b  |->  <.
( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. ) ,  ( x  e.  b ,  y  e.  b  |->  ( h  e.  dom  (
x ( 2nd `  f
) y )  |->  <.
( ( x ( 2nd `  f ) y ) `  h
) ,  ( ( x ( 2nd `  g
) y ) `  h ) >. )
) >.
362, 3, 4, 4, 35cmpt2 5860 . 2  class  ( f  e.  _V ,  g  e.  _V  |->  [_ dom  ( 1st `  f )  /  b ]_ <. ( x  e.  b  |->  <.
( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. ) ,  ( x  e.  b ,  y  e.  b  |->  ( h  e.  dom  (
x ( 2nd `  f
) y )  |->  <.
( ( x ( 2nd `  f ) y ) `  h
) ,  ( ( x ( 2nd `  g
) y ) `  h ) >. )
) >. )
371, 36wceq 1623 1  wff ⟨,⟩F  =  ( f  e. 
_V ,  g  e. 
_V  |->  [_ dom  ( 1st `  f )  /  b ]_ <. ( x  e.  b  |->  <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
) ,  ( x  e.  b ,  y  e.  b  |->  ( h  e.  dom  ( x ( 2nd `  f
) y )  |->  <.
( ( x ( 2nd `  f ) y ) `  h
) ,  ( ( x ( 2nd `  g
) y ) `  h ) >. )
) >. )
Colors of variables: wff set class
This definition is referenced by:  prfval  13973
  Copyright terms: Public domain W3C validator