Metamath Proof Explorer

Theorem idfth

Description: The inclusion functor is a faithful functor. (Contributed by Zhi Wang, 10-Nov-2025)

Ref Expression
Hypothesis idfth.i 
|- I = ( idFunc ` C )
Assertion idfth 
|- ( I e. ( D Func E ) -> I e. ( D Faith E ) )

Proof

Step Hyp Ref Expression
1 idfth.i 
 |-  I = ( idFunc ` C )
2 relfunc 
 |-  Rel ( D Func E )
3 1st2nd 
 |-  ( ( Rel ( D Func E ) /\ I e. ( D Func E ) ) -> I = <. ( 1st ` I ) , ( 2nd ` I ) >. )
4 2 3 mpan 
 |-  ( I e. ( D Func E ) -> I = <. ( 1st ` I ) , ( 2nd ` I ) >. )
5 id 
 |-  ( I e. ( D Func E ) -> I e. ( D Func E ) )
6 5 func1st2nd 
 |-  ( I e. ( D Func E ) -> ( 1st ` I ) ( D Func E ) ( 2nd ` I ) )
7 f1oi 
 |-  ( _I |` ( x ( Hom ` D ) y ) ) : ( x ( Hom ` D ) y ) -1-1-onto-> ( x ( Hom ` D ) y )
8 dff1o3 
 |-  ( ( _I |` ( x ( Hom ` D ) y ) ) : ( x ( Hom ` D ) y ) -1-1-onto-> ( x ( Hom ` D ) y ) <-> ( ( _I |` ( x ( Hom ` D ) y ) ) : ( x ( Hom ` D ) y ) -onto-> ( x ( Hom ` D ) y ) /\ Fun `' ( _I |` ( x ( Hom ` D ) y ) ) ) )
9 7 8 mpbi 
 |-  ( ( _I |` ( x ( Hom ` D ) y ) ) : ( x ( Hom ` D ) y ) -onto-> ( x ( Hom ` D ) y ) /\ Fun `' ( _I |` ( x ( Hom ` D ) y ) ) )
10 9 simpri 
 |-  Fun `' ( _I |` ( x ( Hom ` D ) y ) )
11 simpl 
 |-  ( ( I e. ( D Func E ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> I e. ( D Func E ) )
12 eqidd 
 |-  ( ( I e. ( D Func E ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( Base ` D ) = ( Base ` D ) )
13 simprl 
 |-  ( ( I e. ( D Func E ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> x e. ( Base ` D ) )
14 simprr 
 |-  ( ( I e. ( D Func E ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> y e. ( Base ` D ) )
15 eqidd 
 |-  ( ( I e. ( D Func E ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( x ( Hom ` D ) y ) = ( x ( Hom ` D ) y ) )
16 1 11 12 13 14 15 idfu2nda 
 |-  ( ( I e. ( D Func E ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( x ( 2nd ` I ) y ) = ( _I |` ( x ( Hom ` D ) y ) ) )
17 16 cnveqd 
 |-  ( ( I e. ( D Func E ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> `' ( x ( 2nd ` I ) y ) = `' ( _I |` ( x ( Hom ` D ) y ) ) )
18 17 funeqd 
 |-  ( ( I e. ( D Func E ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( Fun `' ( x ( 2nd ` I ) y ) <-> Fun `' ( _I |` ( x ( Hom ` D ) y ) ) ) )
19 10 18 mpbiri 
 |-  ( ( I e. ( D Func E ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> Fun `' ( x ( 2nd ` I ) y ) )
20 19 ralrimivva 
 |-  ( I e. ( D Func E ) -> A. x e. ( Base ` D ) A. y e. ( Base ` D ) Fun `' ( x ( 2nd ` I ) y ) )
21 eqid 
 |-  ( Base ` D ) = ( Base ` D )
22 21 isfth 
 |-  ( ( 1st ` I ) ( D Faith E ) ( 2nd ` I ) <-> ( ( 1st ` I ) ( D Func E ) ( 2nd ` I ) /\ A. x e. ( Base ` D ) A. y e. ( Base ` D ) Fun `' ( x ( 2nd ` I ) y ) ) )
23 6 20 22 sylanbrc 
 |-  ( I e. ( D Func E ) -> ( 1st ` I ) ( D Faith E ) ( 2nd ` I ) )
24 df-br 
 |-  ( ( 1st ` I ) ( D Faith E ) ( 2nd ` I ) <-> <. ( 1st ` I ) , ( 2nd ` I ) >. e. ( D Faith E ) )
25 23 24 sylib 
 |-  ( I e. ( D Func E ) -> <. ( 1st ` I ) , ( 2nd ` I ) >. e. ( D Faith E ) )
26 4 25 eqeltrd 
 |-  ( I e. ( D Func E ) -> I e. ( D Faith E ) )