Theorem termcnatval

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

	Ref	Expression
Hypotheses	termcnatval.c	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
	termcnatval.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	termcnatval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) )
	termcnatval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	termcnatval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	termcnatval.r	⊢ 𝑅 = ( 𝐴 ‘ 𝑋 )
Assertion	termcnatval	⊢ ( 𝜑 → 𝐴 = { ⟨ 𝑋 , 𝑅 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		termcnatval.c	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
2		termcnatval.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
3		termcnatval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) )
4		termcnatval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
5		termcnatval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		termcnatval.r	⊢ 𝑅 = ( 𝐴 ‘ 𝑋 )
7	2 3	nat1st2nd	⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ 𝑁 ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ ) )
8	2 7 4	natfn	⊢ ( 𝜑 → 𝐴 Fn 𝐵 )
9	1 4 5	termcbas2	⊢ ( 𝜑 → 𝐵 = { 𝑋 } )
10	9	fneq2d	⊢ ( 𝜑 → ( 𝐴 Fn 𝐵 ↔ 𝐴 Fn { 𝑋 } ) )
11	8 10	mpbid	⊢ ( 𝜑 → 𝐴 Fn { 𝑋 } )
12		fnsnbg	⊢ ( 𝑋 ∈ 𝐵 → ( 𝐴 Fn { 𝑋 } ↔ 𝐴 = { ⟨ 𝑋 , ( 𝐴 ‘ 𝑋 ) ⟩ } ) )
13	5 12	syl	⊢ ( 𝜑 → ( 𝐴 Fn { 𝑋 } ↔ 𝐴 = { ⟨ 𝑋 , ( 𝐴 ‘ 𝑋 ) ⟩ } ) )
14	11 13	mpbid	⊢ ( 𝜑 → 𝐴 = { ⟨ 𝑋 , ( 𝐴 ‘ 𝑋 ) ⟩ } )
15	6	opeq2i	⊢ ⟨ 𝑋 , 𝑅 ⟩ = ⟨ 𝑋 , ( 𝐴 ‘ 𝑋 ) ⟩
16	15	sneqi	⊢ { ⟨ 𝑋 , 𝑅 ⟩ } = { ⟨ 𝑋 , ( 𝐴 ‘ 𝑋 ) ⟩ }
17	14 16	eqtr4di	⊢ ( 𝜑 → 𝐴 = { ⟨ 𝑋 , 𝑅 ⟩ } )