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\left[A\right]$$
	imasubc.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
	imasubc.k	$$⊢K=\left(x\in S,y\in S⟼\bigcup _{p\in F^{-1}\left[\left\{x\right\}\right]\times F^{-1}\left[\left\{y\right\}\right]}G\left(p\right)\left[H\left(p\right)\right]\right)$$
	imasubc.f	$$⊢\phi \to F\left(D\mathrm{Full}E\right)G$$
Assertion	imasubc2	$$⊢\phi \to K\in \mathrm{Subcat}\left(E\right)$$

Proof

Step	Hyp	Ref	Expression
1		imasubc.s	$$⊢S=F\left[A\right]$$
2		imasubc.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
3		imasubc.k	$$⊢K=\left(x\in S,y\in S⟼\bigcup _{p\in F^{-1}\left[\left\{x\right\}\right]\times F^{-1}\left[\left\{y\right\}\right]}G\left(p\right)\left[H\left(p\right)\right]\right)$$
4		imasubc.f	$$⊢\phi \to F\left(D\mathrm{Full}E\right)G$$
5		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
6		eqid	$$⊢{\mathrm{Hom}}_{𝑓}\left(E\right)={\mathrm{Hom}}_{𝑓}\left(E\right)$$
7	1 2 3 4 5 6	imasubc	$$⊢\phi \to \left(KFn\left(S\times S\right)\wedge S\subseteq {\mathrm{Base}}_E\wedge {{\mathrm{Hom}}_{𝑓}\left(E\right)\upharpoonright }_{\left(S\times S\right)}=K\right)$$
8	7	simp3d	$$⊢\phi \to {{\mathrm{Hom}}_{𝑓}\left(E\right)\upharpoonright }_{\left(S\times S\right)}=K$$
9		fullfunc	$$⊢D\mathrm{Full}E\subseteq D\mathrm{Func}E$$
10	9	ssbri	$$⊢F\left(D\mathrm{Full}E\right)G\to F\left(D\mathrm{Func}E\right)G$$
11	4 10	syl	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
12	11	funcrcl3	$$⊢\phi \to E\in \mathrm{Cat}$$
13	7	simp2d	$$⊢\phi \to S\subseteq {\mathrm{Base}}_E$$
14	5 6 12 13	fullsubc	$$⊢\phi \to {{\mathrm{Hom}}_{𝑓}\left(E\right)\upharpoonright }_{\left(S\times S\right)}\in \mathrm{Subcat}\left(E\right)$$
15	8 14	eqeltrrd	$$⊢\phi \to K\in \mathrm{Subcat}\left(E\right)$$