This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem idfu2

Description: Value of the morphism part of the identity functor. (Contributed by Mario Carneiro, 28-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 )
idfu2.f 
|- ( ph -> F e. ( X H Y ) )
Assertion idfu2 
|- ( ph -> ( ( X ( 2nd ` I ) Y ) ` F ) = F )

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 idfu2.f 
 |-  ( ph -> F e. ( X H Y ) )
8 1 2 3 4 5 6 idfu2nd 
 |-  ( ph -> ( X ( 2nd ` I ) Y ) = ( _I |` ( X H Y ) ) )
9 8 fveq1d 
 |-  ( ph -> ( ( X ( 2nd ` I ) Y ) ` F ) = ( ( _I |` ( X H Y ) ) ` F ) )
10 fvresi 
 |-  ( F e. ( X H Y ) -> ( ( _I |` ( X H Y ) ) ` F ) = F )
11 7 10 syl 
 |-  ( ph -> ( ( _I |` ( X H Y ) ) ` F ) = F )
12 9 11 eqtrd 
 |-  ( ph -> ( ( X ( 2nd ` I ) Y ) ` F ) = F )