Theorem termcnatval

Description: Value of natural transformations for a terminal category. (Contributed by Zhi Wang, 21-Oct-2025)

	Ref	Expression
Hypotheses	termcnatval.c	No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
	termcnatval.n	$$⊢N=C\mathrm{Nat}D$$
	termcnatval.a	$$⊢\phi \to A\in \left(FNG\right)$$
	termcnatval.b	$$⊢B={\mathrm{Base}}_C$$
	termcnatval.x	$$⊢\phi \to X\in B$$
	termcnatval.r	$$⊢R=A\left(X\right)$$
Assertion	termcnatval	$$⊢\phi \to A=\left\{⟨X,R⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		termcnatval.c	Could not format ( ph -> C e. TermCat ) : No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-
2		termcnatval.n	$$⊢N=C\mathrm{Nat}D$$
3		termcnatval.a	$$⊢\phi \to A\in \left(FNG\right)$$
4		termcnatval.b	$$⊢B={\mathrm{Base}}_C$$
5		termcnatval.x	$$⊢\phi \to X\in B$$
6		termcnatval.r	$$⊢R=A\left(X\right)$$
7	2 3	nat1st2nd	$$⊢\phi \to A\in \left(⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩N⟨1^{st}\left(G\right),2^{nd}\left(G\right)⟩\right)$$
8	2 7 4	natfn	$$⊢\phi \to AFnB$$
9	1 4 5	termcbas2	$$⊢\phi \to B=\left\{X\right\}$$
10	9	fneq2d	$$⊢\phi \to \left(AFnB\leftrightarrow AFn\left\{X\right\}\right)$$
11	8 10	mpbid	$$⊢\phi \to AFn\left\{X\right\}$$
12		fnsnbg	$$⊢X\in B\to \left(AFn\left\{X\right\}\leftrightarrow A=\left\{⟨X,A\left(X\right)⟩\right\}\right)$$
13	5 12	syl	$$⊢\phi \to \left(AFn\left\{X\right\}\leftrightarrow A=\left\{⟨X,A\left(X\right)⟩\right\}\right)$$
14	11 13	mpbid	$$⊢\phi \to A=\left\{⟨X,A\left(X\right)⟩\right\}$$
15	6	opeq2i	$$⊢⟨X,R⟩=⟨X,A\left(X\right)⟩$$
16	15	sneqi	$$⊢\left\{⟨X,R⟩\right\}=\left\{⟨X,A\left(X\right)⟩\right\}$$
17	14 16	eqtr4di	$$⊢\phi \to A=\left\{⟨X,R⟩\right\}$$