Theorem fucoridid

Description: Horizontal composition with the identity natural transformation of the identity functor leaves a natural transformation unchanged. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

	Ref	Expression
Hypotheses	fucoridid.p	No typesetting found for |- ( ph -> ( 2nd ` ( <. C , C >. o.F E ) ) = P ) with typecode |-
	fucoridid.q	$$⊢Q=C\mathrm{FuncCat}C$$
	fucoridid.j	$$⊢J=\mathrm{Id}\left(Q\right)$$
	fucoridid.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
	fucoridid.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	fucoridid.a	$$⊢\phi \to A\in \left(G\left(C\mathrm{Nat}E\right)H\right)$$
Assertion	fucoridid	$$⊢\phi \to A\left(⟨G,I⟩P⟨H,I⟩\right)J\left(I\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		fucoridid.p	Could not format ( ph -> ( 2nd ` ( <. C , C >. o.F E ) ) = P ) : No typesetting found for |- ( ph -> ( 2nd ` ( <. C , C >. o.F E ) ) = P ) with typecode |-
2		fucoridid.q	$$⊢Q=C\mathrm{FuncCat}C$$
3		fucoridid.j	$$⊢J=\mathrm{Id}\left(Q\right)$$
4		fucoridid.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
5		fucoridid.c	$$⊢\phi \to C\in \mathrm{Cat}$$
6		fucoridid.a	$$⊢\phi \to A\in \left(G\left(C\mathrm{Nat}E\right)H\right)$$
7	4	idfucl	$$⊢C\in \mathrm{Cat}\to I\in \left(C\mathrm{Func}C\right)$$
8	5 7	syl	$$⊢\phi \to I\in \left(C\mathrm{Func}C\right)$$
9	1 3 2 6 8	fucorid2	$$⊢\phi \to A\left(⟨G,I⟩P⟨H,I⟩\right)J\left(I\right)=A\circ 1^{st}\left(I\right)$$
10		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
11	4 10 5	idfu1st	$$⊢\phi \to 1^{st}\left(I\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_C}$$
12	11	coeq2d	$$⊢\phi \to A\circ 1^{st}\left(I\right)=A\circ \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_C}\right)$$
13		eqid	$$⊢C\mathrm{Nat}E=C\mathrm{Nat}E$$
14	13 10 6	natfn2	$$⊢\phi \to AFn{\mathrm{Base}}_C$$
15		dffn2	$$⊢AFn{\mathrm{Base}}_C\leftrightarrow A:{\mathrm{Base}}_C⟶\mathrm{V}$$
16	14 15	sylib	$$⊢\phi \to A:{\mathrm{Base}}_C⟶\mathrm{V}$$
17		fcoi1	$$⊢A:{\mathrm{Base}}_C⟶\mathrm{V}\to A\circ \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_C}\right)=A$$
18	16 17	syl	$$⊢\phi \to A\circ \left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_C}\right)=A$$
19	9 12 18	3eqtrd	$$⊢\phi \to A\left(⟨G,I⟩P⟨H,I⟩\right)J\left(I\right)=A$$