Metamath Proof Explorer

Theorem idafval

Description: Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses idafval.i 
|- I = ( IdA ` C )
idafval.b 
|- B = ( Base ` C )
idafval.c 
|- ( ph -> C e. Cat )
idafval.1 
|- .1. = ( Id ` C )
Assertion idafval 
|- ( ph -> I = ( x e. B |-> <. x , x , ( .1. ` x ) >. ) )

Proof

Step Hyp Ref Expression
1 idafval.i 
 |-  I = ( IdA ` C )
2 idafval.b 
 |-  B = ( Base ` C )
3 idafval.c 
 |-  ( ph -> C e. Cat )
4 idafval.1 
 |-  .1. = ( Id ` C )
5 fveq2 
 |-  ( c = C -> ( Base ` c ) = ( Base ` C ) )
6 5 2 eqtr4di 
 |-  ( c = C -> ( Base ` c ) = B )
7 fveq2 
 |-  ( c = C -> ( Id ` c ) = ( Id ` C ) )
8 7 4 eqtr4di 
 |-  ( c = C -> ( Id ` c ) = .1. )
9 8 fveq1d 
 |-  ( c = C -> ( ( Id ` c ) ` x ) = ( .1. ` x ) )
10 9 oteq3d 
 |-  ( c = C -> <. x , x , ( ( Id ` c ) ` x ) >. = <. x , x , ( .1. ` x ) >. )
11 6 10 mpteq12dv 
 |-  ( c = C -> ( x e. ( Base ` c ) |-> <. x , x , ( ( Id ` c ) ` x ) >. ) = ( x e. B |-> <. x , x , ( .1. ` x ) >. ) )
12 df-ida 
 |-  IdA = ( c e. Cat |-> ( x e. ( Base ` c ) |-> <. x , x , ( ( Id ` c ) ` x ) >. ) )
13 11 12 2 mptfvmpt 
 |-  ( C e. Cat -> ( IdA ` C ) = ( x e. B |-> <. x , x , ( .1. ` x ) >. ) )
14 3 13 syl 
 |-  ( ph -> ( IdA ` C ) = ( x e. B |-> <. x , x , ( .1. ` x ) >. ) )
15 1 14 syl5eq 
 |-  ( ph -> I = ( x e. B |-> <. x , x , ( .1. ` x ) >. ) )