Theorem idsubc

Description: The source category of an inclusion functor is a subcategory of the target category. See also Remark 4.4 in Adamek p. 49. (Contributed by Zhi Wang, 10-Nov-2025)

	Ref	Expression
Hypotheses	idfth.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
	idsubc.h	$$⊢H={\mathrm{Hom}}_{𝑓}\left(D\right)$$
Assertion	idsubc	$$⊢I\in \left(D\mathrm{Func}E\right)\to H\in \mathrm{Subcat}\left(E\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		id	$$⊢I\in \left(D\mathrm{Func}E\right)\to I\in \left(D\mathrm{Func}E\right)$$
4		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
5		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)$$
6	1 3	imaidfu2lem	$$⊢I\in \left(D\mathrm{Func}E\right)\to 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]={\mathrm{Base}}_D$$
7	1 3 4 2 5 6	imaidfu2	$$⊢I\in \left(D\mathrm{Func}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)$$
8		eqid	$$⊢1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]=1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]$$
9	3	func1st2nd	$$⊢I\in \left(D\mathrm{Func}E\right)\to 1^{st}\left(I\right)\left(D\mathrm{Func}E\right)2^{nd}\left(I\right)$$
10		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}\right):{\mathrm{Base}}_D\underset{1-1\; onto}{⟶}{\mathrm{Base}}_D$$
11		dff1o3	$$⊢\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}\right):{\mathrm{Base}}_D\underset{1-1\; onto}{⟶}{\mathrm{Base}}_D\leftrightarrow \left(\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}\right):{\mathrm{Base}}_D\underset{onto}{⟶}{\mathrm{Base}}_D\wedge \mathrm{Fun}{\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}\right)}^{-1}\right)$$
12	10 11	mpbi	$$⊢\left(\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}\right):{\mathrm{Base}}_D\underset{onto}{⟶}{\mathrm{Base}}_D\wedge \mathrm{Fun}{\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}\right)}^{-1}\right)$$
13	12	simpri	$$⊢\mathrm{Fun}{\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}\right)}^{-1}$$
14		eqidd	$$⊢I\in \left(D\mathrm{Func}E\right)\to {\mathrm{Base}}_D={\mathrm{Base}}_D$$
15	1 3 14	idfu1sta	$$⊢I\in \left(D\mathrm{Func}E\right)\to 1^{st}\left(I\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}$$
16	15	cnveqd	$$⊢I\in \left(D\mathrm{Func}E\right)\to {1^{st}\left(I\right)}^{-1}={\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}\right)}^{-1}$$
17	16	funeqd	$$⊢I\in \left(D\mathrm{Func}E\right)\to \left(\mathrm{Fun}{1^{st}\left(I\right)}^{-1}\leftrightarrow \mathrm{Fun}{\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}\right)}^{-1}\right)$$
18	13 17	mpbiri	$$⊢I\in \left(D\mathrm{Func}E\right)\to \mathrm{Fun}{1^{st}\left(I\right)}^{-1}$$
19	8 4 5 9 18	imasubc3	$$⊢I\in \left(D\mathrm{Func}E\right)\to \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)\in \mathrm{Subcat}\left(E\right)$$
20	7 19	eqeltrd	$$⊢I\in \left(D\mathrm{Func}E\right)\to H\in \mathrm{Subcat}\left(E\right)$$