Metamath Proof Explorer

Theorem idfurcl

Description: Reverse closure for an identity functor. (Contributed by Zhi Wang, 10-Nov-2025)

Ref Expression
Assertion idfurcl 
|- ( ( idFunc ` C ) e. ( D Func E ) -> C e. Cat )

Proof

Step Hyp Ref Expression
1 opex 
 |-  <. ( _I |` b ) , ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` t ) ` z ) ) ) >. e. _V
2 1 csbex 
 |-  [_ ( Base ` t ) / b ]_ <. ( _I |` b ) , ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` t ) ` z ) ) ) >. e. _V
3 df-idfu 
 |-  idFunc = ( t e. Cat |-> [_ ( Base ` t ) / b ]_ <. ( _I |` b ) , ( z e. ( b X. b ) |-> ( _I |` ( ( Hom ` t ) ` z ) ) ) >. )
4 2 3 dmmpti 
 |-  dom idFunc = Cat
5 relfunc 
 |-  Rel ( D Func E )
6 0nelrel0 
 |-  ( Rel ( D Func E ) -> -. (/) e. ( D Func E ) )
7 5 6 ax-mp 
 |-  -. (/) e. ( D Func E )
8 4 7 ndmfvrcl 
 |-  ( ( idFunc ` C ) e. ( D Func E ) -> C e. Cat )