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

Metamath Proof Explorer

Theorem idfu1st

Description: Value of the object 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 )
Assertion idfu1st 
|- ( ph -> ( 1st ` I ) = ( _I |` B ) )

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 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
5 1 2 3 4 idfuval 
 |-  ( ph -> I = <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( ( Hom ` C ) ` z ) ) ) >. )
6 5 fveq2d 
 |-  ( ph -> ( 1st ` I ) = ( 1st ` <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( ( Hom ` C ) ` z ) ) ) >. ) )
7 2 fvexi 
 |-  B e. _V
8 resiexg 
 |-  ( B e. _V -> ( _I |` B ) e. _V )
9 7 8 ax-mp 
 |-  ( _I |` B ) e. _V
10 7 7 xpex 
 |-  ( B X. B ) e. _V
11 10 mptex 
 |-  ( z e. ( B X. B ) |-> ( _I |` ( ( Hom ` C ) ` z ) ) ) e. _V
12 9 11 op1st 
 |-  ( 1st ` <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( ( Hom ` C ) ` z ) ) ) >. ) = ( _I |` B )
13 6 12 eqtrdi 
 |-  ( ph -> ( 1st ` I ) = ( _I |` B ) )