Metamath Proof Explorer

Theorem 1stf1

Description: Value of the first projection on an object. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses 1stfval.t 
|- T = ( C Xc. D )
1stfval.b 
|- B = ( Base ` T )
1stfval.h 
|- H = ( Hom ` T )
1stfval.c 
|- ( ph -> C e. Cat )
1stfval.d 
|- ( ph -> D e. Cat )
1stfval.p 
|- P = ( C 1stF D )
1stf1.p 
|- ( ph -> R e. B )
Assertion 1stf1 
|- ( ph -> ( ( 1st ` P ) ` R ) = ( 1st ` R ) )

Proof

Step Hyp Ref Expression
1 1stfval.t 
 |-  T = ( C Xc. D )
2 1stfval.b 
 |-  B = ( Base ` T )
3 1stfval.h 
 |-  H = ( Hom ` T )
4 1stfval.c 
 |-  ( ph -> C e. Cat )
5 1stfval.d 
 |-  ( ph -> D e. Cat )
6 1stfval.p 
 |-  P = ( C 1stF D )
7 1stf1.p 
 |-  ( ph -> R e. B )
8 1 2 3 4 5 6 1stfval 
 |-  ( ph -> P = <. ( 1st |` B ) , ( x e. B , y e. B |-> ( 1st |` ( x H y ) ) ) >. )
9 fo1st 
 |-  1st : _V -onto-> _V
10 fofun 
 |-  ( 1st : _V -onto-> _V -> Fun 1st )
11 9 10 ax-mp 
 |-  Fun 1st
12 2 fvexi 
 |-  B e. _V
13 resfunexg 
 |-  ( ( Fun 1st /\ B e. _V ) -> ( 1st |` B ) e. _V )
14 11 12 13 mp2an 
 |-  ( 1st |` B ) e. _V
15 12 12 mpoex 
 |-  ( x e. B , y e. B |-> ( 1st |` ( x H y ) ) ) e. _V
16 14 15 op1std 
 |-  ( P = <. ( 1st |` B ) , ( x e. B , y e. B |-> ( 1st |` ( x H y ) ) ) >. -> ( 1st ` P ) = ( 1st |` B ) )
17 8 16 syl 
 |-  ( ph -> ( 1st ` P ) = ( 1st |` B ) )
18 17 fveq1d 
 |-  ( ph -> ( ( 1st ` P ) ` R ) = ( ( 1st |` B ) ` R ) )
19 7 fvresd 
 |-  ( ph -> ( ( 1st |` B ) ` R ) = ( 1st ` R ) )
20 18 19 eqtrd 
 |-  ( ph -> ( ( 1st ` P ) ` R ) = ( 1st ` R ) )