Theorem fucterm

Description: The category of functors to a terminal category is terminal. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Hypotheses	funcsn.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	fucterm.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	fucterm.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
Assertion	fucterm	⊢ ( 𝜑 → 𝑄 ∈ TermCat )

Proof

Step	Hyp	Ref	Expression
1		funcsn.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		fucterm.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		fucterm.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
4		opex	⊢ ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ ∈ V
5	4	a1i	⊢ ( 𝜑 → ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ ∈ V )
6		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
8		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
10		eqid	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) )
11		eqid	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) )
12	2 3 6 7 8 9 10 11	functermc2	⊢ ( 𝜑 → ( 𝐶 Func 𝐷 ) = { ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ } )
13	3	termcthind	⊢ ( 𝜑 → 𝐷 ∈ ThinCat )
14	1 5 12 13	funcsn	⊢ ( 𝜑 → 𝑄 ∈ TermCat )