This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imasubc2

Description: An image of a full functor is a (full) 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 ) ) )
imasubc.f 
|- ( ph -> F ( D Full E ) G )
Assertion imasubc2 
|- ( 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 imasubc.f 
 |-  ( ph -> F ( D Full E ) G )
5 eqid 
 |-  ( Base ` E ) = ( Base ` E )
6 eqid 
 |-  ( Homf ` E ) = ( Homf ` E )
7 1 2 3 4 5 6 imasubc 
 |-  ( ph -> ( K Fn ( S X. S ) /\ S C_ ( Base ` E ) /\ ( ( Homf ` E ) |` ( S X. S ) ) = K ) )
8 7 simp3d 
 |-  ( ph -> ( ( Homf ` E ) |` ( S X. S ) ) = K )
9 fullfunc 
 |-  ( D Full E ) C_ ( D Func E )
10 9 ssbri 
 |-  ( F ( D Full E ) G -> F ( D Func E ) G )
11 4 10 syl 
 |-  ( ph -> F ( D Func E ) G )
12 11 funcrcl3 
 |-  ( ph -> E e. Cat )
13 7 simp2d 
 |-  ( ph -> S C_ ( Base ` E ) )
14 5 6 12 13 fullsubc 
 |-  ( ph -> ( ( Homf ` E ) |` ( S X. S ) ) e. ( Subcat ` E ) )
15 8 14 eqeltrrd 
 |-  ( ph -> K e. ( Subcat ` E ) )