Theorem termcnatval

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

	Ref	Expression
Hypotheses	termcnatval.c	|- ( ph -> C e. TermCat )
	termcnatval.n	|- N = ( C Nat D )
	termcnatval.a	|- ( ph -> A e. ( F N G ) )
	termcnatval.b	|- B = ( Base ` C )
	termcnatval.x	|- ( ph -> X e. B )
	termcnatval.r	|- R = ( A ` X )
Assertion	termcnatval	|- ( ph -> A = { <. X , R >. } )

Proof

Step	Hyp	Ref	Expression
1		termcnatval.c	|- ( ph -> C e. TermCat )
2		termcnatval.n	|- N = ( C Nat D )
3		termcnatval.a	|- ( ph -> A e. ( F N G ) )
4		termcnatval.b	|- B = ( Base ` C )
5		termcnatval.x	|- ( ph -> X e. B )
6		termcnatval.r	|- R = ( A ` X )
7	2 3	nat1st2nd	|- ( ph -> A e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
8	2 7 4	natfn	|- ( ph -> A Fn B )
9	1 4 5	termcbas2	|- ( ph -> B = { X } )
10	9	fneq2d	|- ( ph -> ( A Fn B <-> A Fn { X } ) )
11	8 10	mpbid	|- ( ph -> A Fn { X } )
12		fnsnbg	|- ( X e. B -> ( A Fn { X } <-> A = { <. X , ( A ` X ) >. } ) )
13	5 12	syl	|- ( ph -> ( A Fn { X } <-> A = { <. X , ( A ` X ) >. } ) )
14	11 13	mpbid	|- ( ph -> A = { <. X , ( A ` X ) >. } )
15	6	opeq2i	|- <. X , R >. = <. X , ( A ` X ) >.
16	15	sneqi	|- { <. X , R >. } = { <. X , ( A ` X ) >. }
17	14 16	eqtr4di	|- ( ph -> A = { <. X , R >. } )