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 ) )