Metamath Proof Explorer

Theorem 2ndf1

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 )
2ndfval.p 
|- Q = ( C 2ndF D )
2ndf1.p 
|- ( ph -> R e. B )
Assertion 2ndf1 
|- ( ph -> ( ( 1st ` Q ) ` R ) = ( 2nd ` 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 2ndfval.p 
 |-  Q = ( C 2ndF D )
7 2ndf1.p 
 |-  ( ph -> R e. B )
8 1 2 3 4 5 6 2ndfval 
 |-  ( ph -> Q = <. ( 2nd |` B ) , ( x e. B , y e. B |-> ( 2nd |` ( x H y ) ) ) >. )
9 fo2nd 
 |-  2nd : _V -onto-> _V
10 fofun 
 |-  ( 2nd : _V -onto-> _V -> Fun 2nd )
11 9 10 ax-mp 
 |-  Fun 2nd
12 2 fvexi 
 |-  B e. _V
13 resfunexg 
 |-  ( ( Fun 2nd /\ B e. _V ) -> ( 2nd |` B ) e. _V )
14 11 12 13 mp2an 
 |-  ( 2nd |` B ) e. _V
15 12 12 mpoex 
 |-  ( x e. B , y e. B |-> ( 2nd |` ( x H y ) ) ) e. _V
16 14 15 op1std 
 |-  ( Q = <. ( 2nd |` B ) , ( x e. B , y e. B |-> ( 2nd |` ( x H y ) ) ) >. -> ( 1st ` Q ) = ( 2nd |` B ) )
17 8 16 syl 
 |-  ( ph -> ( 1st ` Q ) = ( 2nd |` B ) )
18 17 fveq1d 
 |-  ( ph -> ( ( 1st ` Q ) ` R ) = ( ( 2nd |` B ) ` R ) )
19 7 fvresd 
 |-  ( ph -> ( ( 2nd |` B ) ` R ) = ( 2nd ` R ) )
20 18 19 eqtrd 
 |-  ( ph -> ( ( 1st ` Q ) ` R ) = ( 2nd ` R ) )