Theorem imaidfu2

Description: The image of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025)

	Ref	Expression
Hypotheses	imaidfu.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
	imaidfu.d	$$⊢\phi \to I\in \left(D\mathrm{Func}E\right)$$
	imaidfu.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
	imaidfu.j	$$⊢J={\mathrm{Hom}}_{𝑓}\left(D\right)$$
	imaidfu.k	$$⊢K=\left(x\in S,y\in S⟼\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[H\left(p\right)\right]\right)$$
	imaidfu2.s	$$⊢\phi \to S={\mathrm{Base}}_D$$
Assertion	imaidfu2	$$⊢\phi \to J=K$$

Proof

Step	Hyp	Ref	Expression
1		imaidfu.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
2		imaidfu.d	$$⊢\phi \to I\in \left(D\mathrm{Func}E\right)$$
3		imaidfu.h	$$⊢H=\mathrm{Hom}\left(D\right)$$
4		imaidfu.j	$$⊢J={\mathrm{Hom}}_{𝑓}\left(D\right)$$
5		imaidfu.k	$$⊢K=\left(x\in S,y\in S⟼\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[H\left(p\right)\right]\right)$$
6		imaidfu2.s	$$⊢\phi \to S={\mathrm{Base}}_D$$
7		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[H\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[H\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	1 2 3 4 7 8	imaidfu	$$⊢\phi \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[H\left(p\right)\right]\right)$$
10		eqidd	$$⊢\phi \to {\mathrm{Base}}_D={\mathrm{Base}}_D$$
11	1 2 10	idfu1sta	$$⊢\phi \to 1^{st}\left(I\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}$$
12	11	imaeq1d	$$⊢\phi \to 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]=\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}\right)\left[{\mathrm{Base}}_D\right]$$
13		ssid	$$⊢{\mathrm{Base}}_D\subseteq {\mathrm{Base}}_D$$
14		resiima	$$⊢{\mathrm{Base}}_D\subseteq {\mathrm{Base}}_D\to \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}\right)\left[{\mathrm{Base}}_D\right]={\mathrm{Base}}_D$$
15	13 14	ax-mp	$$⊢\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_D}\right)\left[{\mathrm{Base}}_D\right]={\mathrm{Base}}_D$$
16	12 15	eqtrdi	$$⊢\phi \to 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]={\mathrm{Base}}_D$$
17	16	sqxpeqd	$$⊢\phi \to 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]\times 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]={\mathrm{Base}}_D\times {\mathrm{Base}}_D$$
18	17	reseq2d	$$⊢\phi \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)}={J\upharpoonright }_{\left({\mathrm{Base}}_D\times {\mathrm{Base}}_D\right)}$$
19		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
20	4 19	homffn	$$⊢JFn\left({\mathrm{Base}}_D\times {\mathrm{Base}}_D\right)$$
21		fnresdm	$$⊢JFn\left({\mathrm{Base}}_D\times {\mathrm{Base}}_D\right)\to {J\upharpoonright }_{\left({\mathrm{Base}}_D\times {\mathrm{Base}}_D\right)}=J$$
22	20 21	ax-mp	$$⊢{J\upharpoonright }_{\left({\mathrm{Base}}_D\times {\mathrm{Base}}_D\right)}=J$$
23	18 22	eqtrdi	$$⊢\phi \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)}=J$$
24	15 12 6	3eqtr4a	$$⊢\phi \to 1^{st}\left(I\right)\left[{\mathrm{Base}}_D\right]=S$$
25		eqidd	$$⊢\phi \to \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[H\left(p\right)\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[H\left(p\right)\right]$$
26	24 24 25	mpoeq123dv	$$⊢\phi \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[H\left(p\right)\right]\right)=\left(x\in S,y\in S⟼\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[H\left(p\right)\right]\right)$$
27	9 23 26	3eqtr3d	$$⊢\phi \to J=\left(x\in S,y\in S⟼\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[H\left(p\right)\right]\right)$$
28	27 5	eqtr4di	$$⊢\phi \to J=K$$