Metamath Proof Explorer

Theorem idemb

Description: The inclusion functor is an embedding. Remark 4.4(1) in Adamek p. 49. (Contributed by Zhi Wang, 16-Nov-2025)

Ref Expression
Hypothesis idfth.i 
|- I = ( idFunc ` C )
Assertion idemb 
|- ( I e. ( D Func E ) -> ( I e. ( D Faith E ) /\ Fun `' ( 1st ` I ) ) )

Proof

Step Hyp Ref Expression
1 idfth.i 
 |-  I = ( idFunc ` C )
2 1 idfth 
 |-  ( I e. ( D Func E ) -> I e. ( D Faith E ) )
3 1 eleq1i 
 |-  ( I e. ( D Func E ) <-> ( idFunc ` C ) e. ( D Func E ) )
4 idfurcl 
 |-  ( ( idFunc ` C ) e. ( D Func E ) -> C e. Cat )
5 3 4 sylbi 
 |-  ( I e. ( D Func E ) -> C e. Cat )
6 eqid 
 |-  ( Base ` C ) = ( Base ` C )
7 1 6 idfu1stf1o 
 |-  ( C e. Cat -> ( 1st ` I ) : ( Base ` C ) -1-1-onto-> ( Base ` C ) )
8 dff1o4 
 |-  ( ( 1st ` I ) : ( Base ` C ) -1-1-onto-> ( Base ` C ) <-> ( ( 1st ` I ) Fn ( Base ` C ) /\ `' ( 1st ` I ) Fn ( Base ` C ) ) )
9 8 simprbi 
 |-  ( ( 1st ` I ) : ( Base ` C ) -1-1-onto-> ( Base ` C ) -> `' ( 1st ` I ) Fn ( Base ` C ) )
10 5 7 9 3syl 
 |-  ( I e. ( D Func E ) -> `' ( 1st ` I ) Fn ( Base ` C ) )
11 10 fnfund 
 |-  ( I e. ( D Func E ) -> Fun `' ( 1st ` I ) )
12 2 11 jca 
 |-  ( I e. ( D Func E ) -> ( I e. ( D Faith E ) /\ Fun `' ( 1st ` I ) ) )