Metamath Proof Explorer

Theorem prf1

Description: Value of the pairing functor on objects. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses prfval.k 
|- P = ( F pairF G )
prfval.b 
|- B = ( Base ` C )
prfval.h 
|- H = ( Hom ` C )
prfval.c 
|- ( ph -> F e. ( C Func D ) )
prfval.d 
|- ( ph -> G e. ( C Func E ) )
prf1.x 
|- ( ph -> X e. B )
Assertion prf1 
|- ( ph -> ( ( 1st ` P ) ` X ) = <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` X ) >. )

Proof

Step Hyp Ref Expression
1 prfval.k 
 |-  P = ( F pairF G )
2 prfval.b 
 |-  B = ( Base ` C )
3 prfval.h 
 |-  H = ( Hom ` C )
4 prfval.c 
 |-  ( ph -> F e. ( C Func D ) )
5 prfval.d 
 |-  ( ph -> G e. ( C Func E ) )
6 prf1.x 
 |-  ( ph -> X e. B )
7 1 2 3 4 5 prfval 
 |-  ( ph -> P = <. ( x e. B |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) , ( x e. B , y e. B |-> ( h e. ( x H y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) >. )
8 2 fvexi 
 |-  B e. _V
9 8 mptex 
 |-  ( x e. B |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) e. _V
10 8 8 mpoex 
 |-  ( x e. B , y e. B |-> ( h e. ( x H y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) e. _V
11 9 10 op1std 
 |-  ( P = <. ( x e. B |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) , ( x e. B , y e. B |-> ( h e. ( x H y ) |-> <. ( ( x ( 2nd ` F ) y ) ` h ) , ( ( x ( 2nd ` G ) y ) ` h ) >. ) ) >. -> ( 1st ` P ) = ( x e. B |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) )
12 7 11 syl 
 |-  ( ph -> ( 1st ` P ) = ( x e. B |-> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. ) )
13 simpr 
 |-  ( ( ph /\ x = X ) -> x = X )
14 13 fveq2d 
 |-  ( ( ph /\ x = X ) -> ( ( 1st ` F ) ` x ) = ( ( 1st ` F ) ` X ) )
15 13 fveq2d 
 |-  ( ( ph /\ x = X ) -> ( ( 1st ` G ) ` x ) = ( ( 1st ` G ) ` X ) )
16 14 15 opeq12d 
 |-  ( ( ph /\ x = X ) -> <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. = <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` X ) >. )
17 opex 
 |-  <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` X ) >. e. _V
18 17 a1i 
 |-  ( ph -> <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` X ) >. e. _V )
19 12 16 6 18 fvmptd 
 |-  ( ph -> ( ( 1st ` P ) ` X ) = <. ( ( 1st ` F ) ` X ) , ( ( 1st ` G ) ` X ) >. )