Theorem functermceu

Description: There exists a unique functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025)

	Ref	Expression
Hypotheses	functermceu.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	functermceu.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
Assertion	functermceu	⊢ ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		functermceu.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
2		functermceu.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
3		opex	⊢ ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ ∈ V
4	3	a1i	⊢ ( 𝜑 → ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ ∈ V )
5		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
7		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
8		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
9		eqid	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) )
10		eqid	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) )
11	1 2 5 6 7 8 9 10	functermc2	⊢ ( 𝜑 → ( 𝐶 Func 𝐷 ) = { ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ } )
12		sneq	⊢ ( 𝑓 = ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ → { 𝑓 } = { ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ } )
13	12	eqeq2d	⊢ ( 𝑓 = ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ → ( ( 𝐶 Func 𝐷 ) = { 𝑓 } ↔ ( 𝐶 Func 𝐷 ) = { ⟨ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) ‘ 𝑦 ) ) ) ) ⟩ } ) )
14	4 11 13	spcedv	⊢ ( 𝜑 → ∃ 𝑓 ( 𝐶 Func 𝐷 ) = { 𝑓 } )
15		eusn	⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) ↔ ∃ 𝑓 ( 𝐶 Func 𝐷 ) = { 𝑓 } )
16	14 15	sylibr	⊢ ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) )