Metamath Proof Explorer

Theorem idsubc

Description: The source category of an inclusion functor is a subcategory of the target category. See also Remark 4.4 in Adamek p. 49. (Contributed by Zhi Wang, 10-Nov-2025)

Ref Expression
Hypotheses idfth.i 
|- I = ( idFunc ` C )
idsubc.h 
|- H = ( Homf ` D )
Assertion idsubc 
|- ( I e. ( D Func E ) -> H e. ( Subcat ` E ) )

Proof

Step Hyp Ref Expression
1 idfth.i 
 |-  I = ( idFunc ` C )
2 idsubc.h 
 |-  H = ( Homf ` D )
3 id 
 |-  ( I e. ( D Func E ) -> I e. ( D Func E ) )
4 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
5 eqid 
 |-  ( x e. ( ( 1st ` I ) " ( Base ` D ) ) , y e. ( ( 1st ` I ) " ( Base ` D ) ) |-> U_ p e. ( ( `' ( 1st ` I ) " { x } ) X. ( `' ( 1st ` I ) " { y } ) ) ( ( ( 2nd ` I ) ` p ) " ( ( Hom ` D ) ` p ) ) ) = ( x e. ( ( 1st ` I ) " ( Base ` D ) ) , y e. ( ( 1st ` I ) " ( Base ` D ) ) |-> U_ p e. ( ( `' ( 1st ` I ) " { x } ) X. ( `' ( 1st ` I ) " { y } ) ) ( ( ( 2nd ` I ) ` p ) " ( ( Hom ` D ) ` p ) ) )
6 1 3 imaidfu2lem 
 |-  ( I e. ( D Func E ) -> ( ( 1st ` I ) " ( Base ` D ) ) = ( Base ` D ) )
7 1 3 4 2 5 6 imaidfu2 
 |-  ( I e. ( D Func E ) -> H = ( x e. ( ( 1st ` I ) " ( Base ` D ) ) , y e. ( ( 1st ` I ) " ( Base ` D ) ) |-> U_ p e. ( ( `' ( 1st ` I ) " { x } ) X. ( `' ( 1st ` I ) " { y } ) ) ( ( ( 2nd ` I ) ` p ) " ( ( Hom ` D ) ` p ) ) ) )
8 eqid 
 |-  ( ( 1st ` I ) " ( Base ` D ) ) = ( ( 1st ` I ) " ( Base ` D ) )
9 3 func1st2nd 
 |-  ( I e. ( D Func E ) -> ( 1st ` I ) ( D Func E ) ( 2nd ` I ) )
10 f1oi 
 |-  ( _I |` ( Base ` D ) ) : ( Base ` D ) -1-1-onto-> ( Base ` D )
11 dff1o3 
 |-  ( ( _I |` ( Base ` D ) ) : ( Base ` D ) -1-1-onto-> ( Base ` D ) <-> ( ( _I |` ( Base ` D ) ) : ( Base ` D ) -onto-> ( Base ` D ) /\ Fun `' ( _I |` ( Base ` D ) ) ) )
12 10 11 mpbi 
 |-  ( ( _I |` ( Base ` D ) ) : ( Base ` D ) -onto-> ( Base ` D ) /\ Fun `' ( _I |` ( Base ` D ) ) )
13 12 simpri 
 |-  Fun `' ( _I |` ( Base ` D ) )
14 eqidd 
 |-  ( I e. ( D Func E ) -> ( Base ` D ) = ( Base ` D ) )
15 1 3 14 idfu1sta 
 |-  ( I e. ( D Func E ) -> ( 1st ` I ) = ( _I |` ( Base ` D ) ) )
16 15 cnveqd 
 |-  ( I e. ( D Func E ) -> `' ( 1st ` I ) = `' ( _I |` ( Base ` D ) ) )
17 16 funeqd 
 |-  ( I e. ( D Func E ) -> ( Fun `' ( 1st ` I ) <-> Fun `' ( _I |` ( Base ` D ) ) ) )
18 13 17 mpbiri 
 |-  ( I e. ( D Func E ) -> Fun `' ( 1st ` I ) )
19 8 4 5 9 18 imasubc3 
 |-  ( I e. ( D Func E ) -> ( x e. ( ( 1st ` I ) " ( Base ` D ) ) , y e. ( ( 1st ` I ) " ( Base ` D ) ) |-> U_ p e. ( ( `' ( 1st ` I ) " { x } ) X. ( `' ( 1st ` I ) " { y } ) ) ( ( ( 2nd ` I ) ` p ) " ( ( Hom ` D ) ` p ) ) ) e. ( Subcat ` E ) )
20 7 19 eqeltrd 
 |-  ( I e. ( D Func E ) -> H e. ( Subcat ` E ) )