Metamath Proof Explorer

Theorem idfuval

Description: Value 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 )
Assertion idfuval 
|- ( ph -> I = <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) >. )

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 fvexd 
 |-  ( c = C -> ( Base ` c ) e. _V )
6 fveq2 
 |-  ( c = C -> ( Base ` c ) = ( Base ` C ) )
7 6 2 eqtr4di 
 |-  ( c = C -> ( Base ` c ) = B )
8 simpr 
 |-  ( ( c = C /\ b = B ) -> b = B )
9 8 reseq2d 
 |-  ( ( c = C /\ b = B ) -> ( _I |` b ) = ( _I |` B ) )
10 8 sqxpeqd 
 |-  ( ( c = C /\ b = B ) -> ( b X. b ) = ( B X. B ) )
11 simpl 
 |-  ( ( c = C /\ b = B ) -> c = C )
12 11 fveq2d 
 |-  ( ( c = C /\ b = B ) -> ( Hom ` c ) = ( Hom ` C ) )
13 12 4 eqtr4di 
 |-  ( ( c = C /\ b = B ) -> ( Hom ` c ) = H )
14 13 fveq1d 
 |-  ( ( c = C /\ b = B ) -> ( ( Hom ` c ) ` z ) = ( H ` z ) )
15 14 reseq2d 
 |-  ( ( c = C /\ b = B ) -> ( _I |` ( ( Hom ` c ) ` z ) ) = ( _I |` ( H ` z ) ) )
16 10 15 mpteq12dv 
 |-  ( ( c = C /\ b = B ) -> ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` c ) ` z ) ) ) = ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) )
17 9 16 opeq12d 
 |-  ( ( c = C /\ b = B ) -> <. ( _I |` b ) , ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` c ) ` z ) ) ) >. = <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) >. )
18 5 7 17 csbied2 
 |-  ( c = C -> [_ ( Base ` c ) / b ]_ <. ( _I |` b ) , ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` c ) ` z ) ) ) >. = <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) >. )
19 df-idfu 
 |-  idFunc = ( c e. Cat |-> [_ ( Base ` c ) / b ]_ <. ( _I |` b ) , ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` c ) ` z ) ) ) >. )
20 opex 
 |-  <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) >. e. _V
21 18 19 20 fvmpt 
 |-  ( C e. Cat -> ( idFunc ` C ) = <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) >. )
22 3 21 syl 
 |-  ( ph -> ( idFunc ` C ) = <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) >. )
23 1 22 syl5eq 
 |-  ( ph -> I = <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( H ` z ) ) ) >. )