Theorem termcfunc1eq

Description: Functors with terminal source are equal when they agree on its object. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypotheses	termcfunc1eq.c	No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
	termcfunc1eq.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	termcfunc1eq.b	$$⊢B={\mathrm{Base}}_C$$
	termcfunc1eq.g	$$⊢\phi \to G\in \left(C\mathrm{Func}D\right)$$
	termcfunc1eq.y	$$⊢\phi \to Y\in B$$
	termcfunc1eq.e	$$⊢\phi \to 1^{st}\left(F\right)\left(Y\right)=1^{st}\left(G\right)\left(Y\right)$$
Assertion	termcfunc1eq	$$⊢\phi \to F=G$$

Proof

Step	Hyp	Ref	Expression
1		termcfunc1eq.c	Could not format ( ph -> C e. TermCat ) : No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
2		termcfunc1eq.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
3		termcfunc1eq.b	$$⊢B={\mathrm{Base}}_C$$
4		termcfunc1eq.g	$$⊢\phi \to G\in \left(C\mathrm{Func}D\right)$$
5		termcfunc1eq.y	$$⊢\phi \to Y\in B$$
6		termcfunc1eq.e	$$⊢\phi \to 1^{st}\left(F\right)\left(Y\right)=1^{st}\left(G\right)\left(Y\right)$$
7	6	opeq2d	$$⊢\phi \to ⟨Y,1^{st}\left(F\right)\left(Y\right)⟩=⟨Y,1^{st}\left(G\right)\left(Y\right)⟩$$
8	7	sneqd	$$⊢\phi \to \left\{⟨Y,1^{st}\left(F\right)\left(Y\right)⟩\right\}=\left\{⟨Y,1^{st}\left(G\right)\left(Y\right)⟩\right\}$$
9	6	fveq2d	$$⊢\phi \to \mathrm{Id}\left(D\right)\left(1^{st}\left(F\right)\left(Y\right)\right)=\mathrm{Id}\left(D\right)\left(1^{st}\left(G\right)\left(Y\right)\right)$$
10	9	opeq2d	$$⊢\phi \to ⟨\mathrm{Id}\left(C\right)\left(Y\right),\mathrm{Id}\left(D\right)\left(1^{st}\left(F\right)\left(Y\right)\right)⟩=⟨\mathrm{Id}\left(C\right)\left(Y\right),\mathrm{Id}\left(D\right)\left(1^{st}\left(G\right)\left(Y\right)\right)⟩$$
11	10	sneqd	$$⊢\phi \to \left\{⟨\mathrm{Id}\left(C\right)\left(Y\right),\mathrm{Id}\left(D\right)\left(1^{st}\left(F\right)\left(Y\right)\right)⟩\right\}=\left\{⟨\mathrm{Id}\left(C\right)\left(Y\right),\mathrm{Id}\left(D\right)\left(1^{st}\left(G\right)\left(Y\right)\right)⟩\right\}$$
12	11	opeq2d	$$⊢\phi \to ⟨⟨Y,Y⟩,\left\{⟨\mathrm{Id}\left(C\right)\left(Y\right),\mathrm{Id}\left(D\right)\left(1^{st}\left(F\right)\left(Y\right)\right)⟩\right\}⟩=⟨⟨Y,Y⟩,\left\{⟨\mathrm{Id}\left(C\right)\left(Y\right),\mathrm{Id}\left(D\right)\left(1^{st}\left(G\right)\left(Y\right)\right)⟩\right\}⟩$$
13	12	sneqd	$$⊢\phi \to \left\{⟨⟨Y,Y⟩,\left\{⟨\mathrm{Id}\left(C\right)\left(Y\right),\mathrm{Id}\left(D\right)\left(1^{st}\left(F\right)\left(Y\right)\right)⟩\right\}⟩\right\}=\left\{⟨⟨Y,Y⟩,\left\{⟨\mathrm{Id}\left(C\right)\left(Y\right),\mathrm{Id}\left(D\right)\left(1^{st}\left(G\right)\left(Y\right)\right)⟩\right\}⟩\right\}$$
14	8 13	opeq12d	$$⊢\phi \to ⟨\left\{⟨Y,1^{st}\left(F\right)\left(Y\right)⟩\right\},\left\{⟨⟨Y,Y⟩,\left\{⟨\mathrm{Id}\left(C\right)\left(Y\right),\mathrm{Id}\left(D\right)\left(1^{st}\left(F\right)\left(Y\right)\right)⟩\right\}⟩\right\}⟩=⟨\left\{⟨Y,1^{st}\left(G\right)\left(Y\right)⟩\right\},\left\{⟨⟨Y,Y⟩,\left\{⟨\mathrm{Id}\left(C\right)\left(Y\right),\mathrm{Id}\left(D\right)\left(1^{st}\left(G\right)\left(Y\right)\right)⟩\right\}⟩\right\}⟩$$
15		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
16		eqid	$$⊢1^{st}\left(F\right)\left(Y\right)=1^{st}\left(F\right)\left(Y\right)$$
17		eqid	$$⊢\mathrm{Id}\left(D\right)=\mathrm{Id}\left(D\right)$$
18		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
19	15 1 2 3 5 16 17 18	termcfuncval	$$⊢\phi \to \left(1^{st}\left(F\right)\left(Y\right)\in {\mathrm{Base}}_D\wedge F=⟨\left\{⟨Y,1^{st}\left(F\right)\left(Y\right)⟩\right\},\left\{⟨⟨Y,Y⟩,\left\{⟨\mathrm{Id}\left(C\right)\left(Y\right),\mathrm{Id}\left(D\right)\left(1^{st}\left(F\right)\left(Y\right)\right)⟩\right\}⟩\right\}⟩\right)$$
20	19	simprd	$$⊢\phi \to F=⟨\left\{⟨Y,1^{st}\left(F\right)\left(Y\right)⟩\right\},\left\{⟨⟨Y,Y⟩,\left\{⟨\mathrm{Id}\left(C\right)\left(Y\right),\mathrm{Id}\left(D\right)\left(1^{st}\left(F\right)\left(Y\right)\right)⟩\right\}⟩\right\}⟩$$
21		eqid	$$⊢1^{st}\left(G\right)\left(Y\right)=1^{st}\left(G\right)\left(Y\right)$$
22	15 1 4 3 5 21 17 18	termcfuncval	$$⊢\phi \to \left(1^{st}\left(G\right)\left(Y\right)\in {\mathrm{Base}}_D\wedge G=⟨\left\{⟨Y,1^{st}\left(G\right)\left(Y\right)⟩\right\},\left\{⟨⟨Y,Y⟩,\left\{⟨\mathrm{Id}\left(C\right)\left(Y\right),\mathrm{Id}\left(D\right)\left(1^{st}\left(G\right)\left(Y\right)\right)⟩\right\}⟩\right\}⟩\right)$$
23	22	simprd	$$⊢\phi \to G=⟨\left\{⟨Y,1^{st}\left(G\right)\left(Y\right)⟩\right\},\left\{⟨⟨Y,Y⟩,\left\{⟨\mathrm{Id}\left(C\right)\left(Y\right),\mathrm{Id}\left(D\right)\left(1^{st}\left(G\right)\left(Y\right)\right)⟩\right\}⟩\right\}⟩$$
24	14 20 23	3eqtr4d	$$⊢\phi \to F=G$$