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={id}_{\mathrm{func}}\left(C\right)$$
	idsubc.h	$$⊢H={\mathrm{Hom}}_{𝑓}\left(D\right)$$
	idfullsubc.j	$$⊢J={\mathrm{Hom}}_{𝑓}\left(E\right)$$
	idfullsubc.b	$$⊢B={\mathrm{Base}}_D$$
	idfullsubc.c	$$⊢C={\mathrm{Base}}_E$$
Assertion	idfullsubc	$$⊢I\in \left(D\mathrm{Full}E\right)\to \left(B\subseteq C\wedge {J\upharpoonright }_{\left(B\times B\right)}=H\right)$$

Proof

Step	Hyp	Ref	Expression
1		idfth.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
2		idsubc.h	$$⊢H={\mathrm{Hom}}_{𝑓}\left(D\right)$$
3		idfullsubc.j	$$⊢J={\mathrm{Hom}}_{𝑓}\left(E\right)$$
4		idfullsubc.b	$$⊢B={\mathrm{Base}}_D$$
5		idfullsubc.c	$$⊢C={\mathrm{Base}}_E$$
6		fullfunc	$$⊢D\mathrm{Full}E\subseteq D\mathrm{Func}E$$
7	6	sseli	$$⊢I\in \left(D\mathrm{Full}E\right)\to I\in \left(D\mathrm{Func}E\right)$$
8	1 7	imaidfu2lem	$$⊢I\in \left(D\mathrm{Full}E\right)\to 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]={\mathrm{Base}}_D$$
9	4 8	eqtr4id	$$⊢I\in \left(D\mathrm{Full}E\right)\to B=1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]$$
10		eqid	$$⊢1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]=1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]$$
11		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
12		eqid	$$⊢\left(x\in 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right],y\in 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]⟼\bigcup _{p\in {1^{st}\left(I\right)}^{-1}\left[\left\{x\right\}\right]\times {1^{st}\left(I\right)}^{-1}\left[\left\{y\right\}\right]}{2}^{nd}\left(I\right)\left(p\right)\left[\mathrm{Hom}\left(D\right)\left(p\right)\right]\right)=\left(x\in 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right],y\in 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]⟼\bigcup _{p\in {1^{st}\left(I\right)}^{-1}\left[\left\{x\right\}\right]\times {1^{st}\left(I\right)}^{-1}\left[\left\{y\right\}\right]}{2}^{nd}\left(I\right)\left(p\right)\left[\mathrm{Hom}\left(D\right)\left(p\right)\right]\right)$$
13		relfull	$$⊢\mathrm{Rel}\left(D\mathrm{Full}E\right)$$
14		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(D\mathrm{Full}E\right)\wedge I\in \left(D\mathrm{Full}E\right)\right)\to 1^{st}\left(I\right)\left(D\mathrm{Full}E\right)2^{nd}\left(I\right)$$
15	13 14	mpan	$$⊢I\in \left(D\mathrm{Full}E\right)\to 1^{st}\left(I\right)\left(D\mathrm{Full}E\right)2^{nd}\left(I\right)$$
16	10 11 12 15 5 3	imasubc	$$⊢I\in \left(D\mathrm{Full}E\right)\to \left(\left(x\in 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right],y\in 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]⟼\bigcup _{p\in {1^{st}\left(I\right)}^{-1}\left[\left\{x\right\}\right]\times {1^{st}\left(I\right)}^{-1}\left[\left\{y\right\}\right]}{2}^{nd}\left(I\right)\left(p\right)\left[\mathrm{Hom}\left(D\right)\left(p\right)\right]\right)Fn\left(1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]\times 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]\right)\wedge 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]\subseteq C\wedge {J\upharpoonright }_{\left(1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]\times 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]\right)}=\left(x\in 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right],y\in 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]⟼\bigcup _{p\in {1^{st}\left(I\right)}^{-1}\left[\left\{x\right\}\right]\times {1^{st}\left(I\right)}^{-1}\left[\left\{y\right\}\right]}{2}^{nd}\left(I\right)\left(p\right)\left[\mathrm{Hom}\left(D\right)\left(p\right)\right]\right)\right)$$
17	16	simp2d	$$⊢I\in \left(D\mathrm{Full}E\right)\to 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]\subseteq C$$
18	9 17	eqsstrd	$$⊢I\in \left(D\mathrm{Full}E\right)\to B\subseteq C$$
19	16	simp3d	$$⊢I\in \left(D\mathrm{Full}E\right)\to {J\upharpoonright }_{\left(1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]\times 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]\right)}=\left(x\in 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right],y\in 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]⟼\bigcup _{p\in {1^{st}\left(I\right)}^{-1}\left[\left\{x\right\}\right]\times {1^{st}\left(I\right)}^{-1}\left[\left\{y\right\}\right]}{2}^{nd}\left(I\right)\left(p\right)\left[\mathrm{Hom}\left(D\right)\left(p\right)\right]\right)$$
20	9	sqxpeqd	$$⊢I\in \left(D\mathrm{Full}E\right)\to B\times B=1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]\times 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]$$
21	20	reseq2d	$$⊢I\in \left(D\mathrm{Full}E\right)\to {J\upharpoonright }_{\left(B\times B\right)}={J\upharpoonright }_{\left(1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]\times 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]\right)}$$
22	1 7 11 2 12 8	imaidfu2	$$⊢I\in \left(D\mathrm{Full}E\right)\to H=\left(x\in 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right],y\in 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]⟼\bigcup _{p\in {1^{st}\left(I\right)}^{-1}\left[\left\{x\right\}\right]\times {1^{st}\left(I\right)}^{-1}\left[\left\{y\right\}\right]}{2}^{nd}\left(I\right)\left(p\right)\left[\mathrm{Hom}\left(D\right)\left(p\right)\right]\right)$$
23	19 21 22	3eqtr4d	$$⊢I\in \left(D\mathrm{Full}E\right)\to {J\upharpoonright }_{\left(B\times B\right)}=H$$
24	18 23	jca	$$⊢I\in \left(D\mathrm{Full}E\right)\to \left(B\subseteq C\wedge {J\upharpoonright }_{\left(B\times B\right)}=H\right)$$