Metamath Proof Explorer

Theorem imasubc3

Description: An image of a functor injective on objects is a subcategory. Remark 4.2(3) of Adamek p. 48. (Contributed by Zhi Wang, 7-Nov-2025)

Ref Expression
Hypotheses imasubc.s 
|- S = ( F " A )
imasubc.h 
|- H = ( Hom ` D )
imasubc.k 
|- K = ( x e. S , y e. S |-> U_ p e. ( ( `' F " { x } ) X. ( `' F " { y } ) ) ( ( G ` p ) " ( H ` p ) ) )
imassc.f 
|- ( ph -> F ( D Func E ) G )
imasubc3.f 
|- ( ph -> Fun `' F )
Assertion imasubc3 
|- ( ph -> K e. ( Subcat ` E ) )

Proof

Step Hyp Ref Expression
1 imasubc.s 
 |-  S = ( F " A )
2 imasubc.h 
 |-  H = ( Hom ` D )
3 imasubc.k 
 |-  K = ( x e. S , y e. S |-> U_ p e. ( ( `' F " { x } ) X. ( `' F " { y } ) ) ( ( G ` p ) " ( H ` p ) ) )
4 imassc.f 
 |-  ( ph -> F ( D Func E ) G )
5 imasubc3.f 
 |-  ( ph -> Fun `' F )
6 eqid 
 |-  ( Homf ` E ) = ( Homf ` E )
7 1 2 3 4 6 imassc 
 |-  ( ph -> K C_cat ( Homf ` E ) )
8 4 adantr 
 |-  ( ( ph /\ a e. S ) -> F ( D Func E ) G )
9 eqid 
 |-  ( Id ` E ) = ( Id ` E )
10 simpr 
 |-  ( ( ph /\ a e. S ) -> a e. S )
11 1 2 3 8 9 10 imaid 
 |-  ( ( ph /\ a e. S ) -> ( ( Id ` E ) ` a ) e. ( a K a ) )
12 4 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a K b ) /\ g e. ( b K c ) ) ) -> F ( D Func E ) G )
13 eqid 
 |-  ( Base ` D ) = ( Base ` D )
14 eqid 
 |-  ( Base ` E ) = ( Base ` E )
15 eqid 
 |-  ( comp ` E ) = ( comp ` E )
16 13 14 4 funcf1 
 |-  ( ph -> F : ( Base ` D ) --> ( Base ` E ) )
17 df-f1 
 |-  ( F : ( Base ` D ) -1-1-> ( Base ` E ) <-> ( F : ( Base ` D ) --> ( Base ` E ) /\ Fun `' F ) )
18 16 5 17 sylanbrc 
 |-  ( ph -> F : ( Base ` D ) -1-1-> ( Base ` E ) )
19 18 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a K b ) /\ g e. ( b K c ) ) ) -> F : ( Base ` D ) -1-1-> ( Base ` E ) )
20 simpllr 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a K b ) /\ g e. ( b K c ) ) ) -> a e. S )
21 simplrl 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a K b ) /\ g e. ( b K c ) ) ) -> b e. S )
22 simplrr 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a K b ) /\ g e. ( b K c ) ) ) -> c e. S )
23 simprl 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a K b ) /\ g e. ( b K c ) ) ) -> f e. ( a K b ) )
24 simprr 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a K b ) /\ g e. ( b K c ) ) ) -> g e. ( b K c ) )
25 1 2 3 12 13 14 15 19 20 21 22 23 24 imaf1co 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a K b ) /\ g e. ( b K c ) ) ) -> ( g ( <. a , b >. ( comp ` E ) c ) f ) e. ( a K c ) )
26 25 ralrimivva 
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) -> A. f e. ( a K b ) A. g e. ( b K c ) ( g ( <. a , b >. ( comp ` E ) c ) f ) e. ( a K c ) )
27 26 ralrimivva 
 |-  ( ( ph /\ a e. S ) -> A. b e. S A. c e. S A. f e. ( a K b ) A. g e. ( b K c ) ( g ( <. a , b >. ( comp ` E ) c ) f ) e. ( a K c ) )
28 11 27 jca 
 |-  ( ( ph /\ a e. S ) -> ( ( ( Id ` E ) ` a ) e. ( a K a ) /\ A. b e. S A. c e. S A. f e. ( a K b ) A. g e. ( b K c ) ( g ( <. a , b >. ( comp ` E ) c ) f ) e. ( a K c ) ) )
29 28 ralrimiva 
 |-  ( ph -> A. a e. S ( ( ( Id ` E ) ` a ) e. ( a K a ) /\ A. b e. S A. c e. S A. f e. ( a K b ) A. g e. ( b K c ) ( g ( <. a , b >. ( comp ` E ) c ) f ) e. ( a K c ) ) )
30 4 funcrcl3 
 |-  ( ph -> E e. Cat )
31 relfunc 
 |-  Rel ( D Func E )
32 31 brrelex1i 
 |-  ( F ( D Func E ) G -> F e. _V )
33 4 32 syl 
 |-  ( ph -> F e. _V )
34 33 33 3 imasubclem2 
 |-  ( ph -> K Fn ( S X. S ) )
35 6 9 15 30 34 issubc2 
 |-  ( ph -> ( K e. ( Subcat ` E ) <-> ( K C_cat ( Homf ` E ) /\ A. a e. S ( ( ( Id ` E ) ` a ) e. ( a K a ) /\ A. b e. S A. c e. S A. f e. ( a K b ) A. g e. ( b K c ) ( g ( <. a , b >. ( comp ` E ) c ) f ) e. ( a K c ) ) ) ) )
36 7 29 35 mpbir2and 
 |-  ( ph -> K e. ( Subcat ` E ) )