Theorem termcterm

Description: A terminal category is a terminal object of the category of small categories. (Contributed by Zhi Wang, 17-Oct-2025)

	Ref	Expression
Hypotheses	termcterm.e	⊢ 𝐸 = ( CatCat ‘ 𝑈 )
	termcterm.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	termcterm.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
	termcterm.t	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
Assertion	termcterm	⊢ ( 𝜑 → 𝐶 ∈ ( TermO ‘ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		termcterm.e	⊢ 𝐸 = ( CatCat ‘ 𝑈 )
2		termcterm.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3		termcterm.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
4		termcterm.t	⊢ ( 𝜑 → 𝐶 ∈ TermCat )
5		simpr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → 𝑑 ∈ ( Base ‘ 𝐸 ) )
6		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
7	1 6 2	catcbas	⊢ ( 𝜑 → ( Base ‘ 𝐸 ) = ( 𝑈 ∩ Cat ) )
8	7	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → ( Base ‘ 𝐸 ) = ( 𝑈 ∩ Cat ) )
9	5 8	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → 𝑑 ∈ ( 𝑈 ∩ Cat ) )
10	9	elin2d	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → 𝑑 ∈ Cat )
11	4	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → 𝐶 ∈ TermCat )
12	10 11	functermceu	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) )
13	2	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → 𝑈 ∈ 𝑉 )
14		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
15	4	termccd	⊢ ( 𝜑 → 𝐶 ∈ Cat )
16	3 15	elind	⊢ ( 𝜑 → 𝐶 ∈ ( 𝑈 ∩ Cat ) )
17	16 7	eleqtrrd	⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ 𝐸 ) )
18	17	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → 𝐶 ∈ ( Base ‘ 𝐸 ) )
19	1 6 13 14 5 18	catchom	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → ( 𝑑 ( Hom ‘ 𝐸 ) 𝐶 ) = ( 𝑑 Func 𝐶 ) )
20	19	eleq2d	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → ( 𝑓 ∈ ( 𝑑 ( Hom ‘ 𝐸 ) 𝐶 ) ↔ 𝑓 ∈ ( 𝑑 Func 𝐶 ) ) )
21	20	eubidv	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → ( ∃! 𝑓 𝑓 ∈ ( 𝑑 ( Hom ‘ 𝐸 ) 𝐶 ) ↔ ∃! 𝑓 𝑓 ∈ ( 𝑑 Func 𝐶 ) ) )
22	12 21	mpbird	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( Base ‘ 𝐸 ) ) → ∃! 𝑓 𝑓 ∈ ( 𝑑 ( Hom ‘ 𝐸 ) 𝐶 ) )
23	22	ralrimiva	⊢ ( 𝜑 → ∀ 𝑑 ∈ ( Base ‘ 𝐸 ) ∃! 𝑓 𝑓 ∈ ( 𝑑 ( Hom ‘ 𝐸 ) 𝐶 ) )
24	1	catccat	⊢ ( 𝑈 ∈ 𝑉 → 𝐸 ∈ Cat )
25	2 24	syl	⊢ ( 𝜑 → 𝐸 ∈ Cat )
26	6 14 25 17	istermo	⊢ ( 𝜑 → ( 𝐶 ∈ ( TermO ‘ 𝐸 ) ↔ ∀ 𝑑 ∈ ( Base ‘ 𝐸 ) ∃! 𝑓 𝑓 ∈ ( 𝑑 ( Hom ‘ 𝐸 ) 𝐶 ) ) )
27	23 26	mpbird	⊢ ( 𝜑 → 𝐶 ∈ ( TermO ‘ 𝐸 ) )