Metamath Proof Explorer

Theorem idfu2nd

Description: Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses idfuval.i 
|- I = ( idFunc ` C )
idfuval.b 
|- B = ( Base ` C )
idfuval.c 
|- ( ph -> C e. Cat )
idfuval.h 
|- H = ( Hom ` C )
idfu2nd.x 
|- ( ph -> X e. B )
idfu2nd.y 
|- ( ph -> Y e. B )
Assertion idfu2nd 
|- ( ph -> ( X ( 2nd ` I ) Y ) = ( _I |` ( X H Y ) ) )

Proof

Step Hyp Ref Expression
1 idfuval.i 
 |-  I = ( idFunc ` C )
2 idfuval.b 
 |-  B = ( Base ` C )
3 idfuval.c 
 |-  ( ph -> C e. Cat )
4 idfuval.h 
 |-  H = ( Hom ` C )
5 idfu2nd.x 
 |-  ( ph -> X e. B )
6 idfu2nd.y 
 |-  ( ph -> Y e. B )
7 df-ov 
 |-  ( X ( 2nd ` I ) Y ) = ( ( 2nd ` I ) ` <. X , Y >. )
8 1 2 3 4 idfuval 
 |-  ( ph -> I = <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) >. )
9 8 fveq2d 
 |-  ( ph -> ( 2nd ` I ) = ( 2nd ` <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) >. ) )
10 2 fvexi 
 |-  B e. _V
11 resiexg 
 |-  ( B e. _V -> ( _I |` B ) e. _V )
12 10 11 ax-mp 
 |-  ( _I |` B ) e. _V
13 10 10 xpex 
 |-  ( B X. B ) e. _V
14 13 mptex 
 |-  ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) e. _V
15 12 14 op2nd 
 |-  ( 2nd ` <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) >. ) = ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) )
16 9 15 eqtrdi 
 |-  ( ph -> ( 2nd ` I ) = ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) )
17 simpr 
 |-  ( ( ph /\ z = <. X , Y >. ) -> z = <. X , Y >. )
18 17 fveq2d 
 |-  ( ( ph /\ z = <. X , Y >. ) -> ( H ` z ) = ( H ` <. X , Y >. ) )
19 df-ov 
 |-  ( X H Y ) = ( H ` <. X , Y >. )
20 18 19 eqtr4di 
 |-  ( ( ph /\ z = <. X , Y >. ) -> ( H ` z ) = ( X H Y ) )
21 20 reseq2d 
 |-  ( ( ph /\ z = <. X , Y >. ) -> ( _I |` ( H ` z ) ) = ( _I |` ( X H Y ) ) )
22 5 6 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( B X. B ) )
23 ovex 
 |-  ( X H Y ) e. _V
24 resiexg 
 |-  ( ( X H Y ) e. _V -> ( _I |` ( X H Y ) ) e. _V )
25 23 24 mp1i 
 |-  ( ph -> ( _I |` ( X H Y ) ) e. _V )
26 16 21 22 25 fvmptd 
 |-  ( ph -> ( ( 2nd ` I ) ` <. X , Y >. ) = ( _I |` ( X H Y ) ) )
27 7 26 syl5eq 
 |-  ( ph -> ( X ( 2nd ` I ) Y ) = ( _I |` ( X H Y ) ) )