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

Metamath Proof Explorer

Theorem idfu1a

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 ) )
idfu2nda.x 
|- ( ph -> X e. B )
Assertion idfu1a 
|- ( ph -> ( ( 1st ` I ) ` X ) = X )

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 idfu2nda.x 
 |-  ( ph -> X e. B )
5 eqid 
 |-  ( Base ` C ) = ( Base ` C )
6 1 2 eqeltrrid 
 |-  ( ph -> ( idFunc ` C ) e. ( D Func E ) )
7 idfurcl 
 |-  ( ( idFunc ` C ) e. ( D Func E ) -> C e. Cat )
8 6 7 syl 
 |-  ( ph -> C e. Cat )
9 1 2 3 idfu1stalem 
 |-  ( ph -> B = ( Base ` C ) )
10 4 9 eleqtrd 
 |-  ( ph -> X e. ( Base ` C ) )
11 1 5 8 10 idfu1 
 |-  ( ph -> ( ( 1st ` I ) ` X ) = X )