Metamath Proof Explorer

Definition df-prf

Description: Define the pairing operation for functors (which takes two functors F : C --> D and G : C --> E and produces ( F pairF G ) : C --> ( D Xc. E ) ). (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Assertion df-prf 
|- pairF = ( 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 ) >. ) ) >. )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprf 
 |-  pairF
1 vf 
 |-  f
2 cvv 
 |-  _V
3 vg 
 |-  g
4 c1st 
 |-  1st
5 1 cv 
 |-  f
6 5 4 cfv 
 |-  ( 1st ` f )
7 6 cdm 
 |-  dom ( 1st ` f )
8 vb 
 |-  b
9 vx 
 |-  x
10 8 cv 
 |-  b
11 9 cv 
 |-  x
12 11 6 cfv 
 |-  ( ( 1st ` f ) ` x )
13 3 cv 
 |-  g
14 13 4 cfv 
 |-  ( 1st ` g )
15 11 14 cfv 
 |-  ( ( 1st ` g ) ` x )
16 12 15 cop 
 |-  <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >.
17 9 10 16 cmpt 
 |-  ( x e. b |-> <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. )
18 vy 
 |-  y
19 vh 
 |-  h
20 c2nd 
 |-  2nd
21 5 20 cfv 
 |-  ( 2nd ` f )
22 18 cv 
 |-  y
23 11 22 21 co 
 |-  ( x ( 2nd ` f ) y )
24 23 cdm 
 |-  dom ( x ( 2nd ` f ) y )
25 19 cv 
 |-  h
26 25 23 cfv 
 |-  ( ( x ( 2nd ` f ) y ) ` h )
27 13 20 cfv 
 |-  ( 2nd ` g )
28 11 22 27 co 
 |-  ( x ( 2nd ` g ) y )
29 25 28 cfv 
 |-  ( ( x ( 2nd ` g ) y ) ` h )
30 26 29 cop 
 |-  <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >.
31 19 24 30 cmpt 
 |-  ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. )
32 9 18 10 10 31 cmpo 
 |-  ( x e. b , y e. b |-> ( h e. dom ( x ( 2nd ` f ) y ) |-> <. ( ( x ( 2nd ` f ) y ) ` h ) , ( ( x ( 2nd ` g ) y ) ` h ) >. ) )
33 17 32 cop 
 |-  <. ( 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 ) >. ) ) >.
34 8 7 33 csb 
 |-  [_ 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 ) >. ) ) >.
35 1 3 2 2 34 cmpo 
 |-  ( 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 ) >. ) ) >. )
36 0 35 wceq 
 |-  pairF = ( 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 ) >. ) ) >. )