Metamath Proof Explorer

Theorem idfullsubc

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

Ref Expression
Hypotheses idfth.i 
|- I = ( idFunc ` C )
idsubc.h 
|- H = ( Homf ` D )
idfullsubc.j 
|- J = ( Homf ` E )
idfullsubc.b 
|- B = ( Base ` D )
idfullsubc.c 
|- C = ( Base ` E )
Assertion idfullsubc 
|- ( I e. ( D Full E ) -> ( B C_ C /\ ( J |` ( B X. B ) ) = H ) )

Proof

Step Hyp Ref Expression
1 idfth.i 
 |-  I = ( idFunc ` C )
2 idsubc.h 
 |-  H = ( Homf ` D )
3 idfullsubc.j 
 |-  J = ( Homf ` E )
4 idfullsubc.b 
 |-  B = ( Base ` D )
5 idfullsubc.c 
 |-  C = ( Base ` E )
6 fullfunc 
 |-  ( D Full E ) C_ ( D Func E )
7 6 sseli 
 |-  ( I e. ( D Full E ) -> I e. ( D Func E ) )
8 1 7 imaidfu2lem 
 |-  ( I e. ( D Full E ) -> ( ( 1st ` I ) " ( Base ` D ) ) = ( Base ` D ) )
9 4 8 eqtr4id 
 |-  ( I e. ( D Full E ) -> B = ( ( 1st ` I ) " ( Base ` D ) ) )
10 eqid 
 |-  ( ( 1st ` I ) " ( Base ` D ) ) = ( ( 1st ` I ) " ( Base ` D ) )
11 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
12 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 ) ) )
13 relfull 
 |-  Rel ( D Full E )
14 1st2ndbr 
 |-  ( ( Rel ( D Full E ) /\ I e. ( D Full E ) ) -> ( 1st ` I ) ( D Full E ) ( 2nd ` I ) )
15 13 14 mpan 
 |-  ( I e. ( D Full E ) -> ( 1st ` I ) ( D Full E ) ( 2nd ` I ) )
16 10 11 12 15 5 3 imasubc 
 |-  ( I e. ( D Full 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 ) ) ) Fn ( ( ( 1st ` I ) " ( Base ` D ) ) X. ( ( 1st ` I ) " ( Base ` D ) ) ) /\ ( ( 1st ` I ) " ( Base ` D ) ) C_ C /\ ( J |` ( ( ( 1st ` I ) " ( Base ` D ) ) X. ( ( 1st ` I ) " ( Base ` D ) ) ) ) = ( 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 ) ) ) ) )
17 16 simp2d 
 |-  ( I e. ( D Full E ) -> ( ( 1st ` I ) " ( Base ` D ) ) C_ C )
18 9 17 eqsstrd 
 |-  ( I e. ( D Full E ) -> B C_ C )
19 16 simp3d 
 |-  ( I e. ( D Full E ) -> ( J |` ( ( ( 1st ` I ) " ( Base ` D ) ) X. ( ( 1st ` I ) " ( Base ` D ) ) ) ) = ( 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 ) ) ) )
20 9 sqxpeqd 
 |-  ( I e. ( D Full E ) -> ( B X. B ) = ( ( ( 1st ` I ) " ( Base ` D ) ) X. ( ( 1st ` I ) " ( Base ` D ) ) ) )
21 20 reseq2d 
 |-  ( I e. ( D Full E ) -> ( J |` ( B X. B ) ) = ( J |` ( ( ( 1st ` I ) " ( Base ` D ) ) X. ( ( 1st ` I ) " ( Base ` D ) ) ) ) )
22 1 7 11 2 12 8 imaidfu2 
 |-  ( I e. ( D Full 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 ) ) ) )
23 19 21 22 3eqtr4d 
 |-  ( I e. ( D Full E ) -> ( J |` ( B X. B ) ) = H )
24 18 23 jca 
 |-  ( I e. ( D Full E ) -> ( B C_ C /\ ( J |` ( B X. B ) ) = H ) )