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

Metamath Proof Explorer

Theorem idfu1sta

Description: Value of the object part of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025)

Ref Expression
Hypotheses idfu2nda.i 
|- I = ( idFunc ` C )
idfu2nda.d 
|- ( ph -> I e. ( D Func E ) )
idfu2nda.b 
|- ( ph -> B = ( Base ` D ) )
Assertion idfu1sta 
|- ( ph -> ( 1st ` I ) = ( _I |` B ) )

Proof

Step Hyp Ref Expression
1 idfu2nda.i 
 |-  I = ( idFunc ` C )
2 idfu2nda.d 
 |-  ( ph -> I e. ( D Func E ) )
3 idfu2nda.b 
 |-  ( ph -> B = ( Base ` D ) )
4 eqid 
 |-  ( Base ` C ) = ( Base ` C )
5 1 2 eqeltrrid 
 |-  ( ph -> ( idFunc ` C ) e. ( D Func E ) )
6 idfurcl 
 |-  ( ( idFunc ` C ) e. ( D Func E ) -> C e. Cat )
7 5 6 syl 
 |-  ( ph -> C e. Cat )
8 1 4 7 idfu1st 
 |-  ( ph -> ( 1st ` I ) = ( _I |` ( Base ` C ) ) )
9 1 2 3 idfu1stalem 
 |-  ( ph -> B = ( Base ` C ) )
10 9 reseq2d 
 |-  ( ph -> ( _I |` B ) = ( _I |` ( Base ` C ) ) )
11 8 10 eqtr4d 
 |-  ( ph -> ( 1st ` I ) = ( _I |` B ) )