Theorem termcterm3

Description: In the category of small categories, a terminal object is equivalent to a terminal category. (Contributed by Zhi Wang, 18-Oct-2025)

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

Proof

Step	Hyp	Ref	Expression
1		termcterm.e	⊢ 𝐸 = ( CatCat ‘ 𝑈 )
2		termcterm3.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
3		termcterm3.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
4		termcterm3.1	⊢ ( 𝜑 → ( SetCat ‘ 1o ) ∈ 𝑈 )
5	2	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ TermCat ) → 𝑈 ∈ 𝑉 )
6	3	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ TermCat ) → 𝐶 ∈ 𝑈 )
7		simpr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ TermCat ) → 𝐶 ∈ TermCat )
8	1 5 6 7	termcterm	⊢ ( ( 𝜑 ∧ 𝐶 ∈ TermCat ) → 𝐶 ∈ ( TermO ‘ 𝐸 ) )
9		setc1oterm	⊢ ( SetCat ‘ 1o ) ∈ TermCat
10	9	a1i	⊢ ( 𝜑 → ( SetCat ‘ 1o ) ∈ TermCat )
11	4 10	elind	⊢ ( 𝜑 → ( SetCat ‘ 1o ) ∈ ( 𝑈 ∩ TermCat ) )
12	11	ne0d	⊢ ( 𝜑 → ( 𝑈 ∩ TermCat ) ≠ ∅ )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( TermO ‘ 𝐸 ) ) → ( 𝑈 ∩ TermCat ) ≠ ∅ )
14		simpr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( TermO ‘ 𝐸 ) ) → 𝐶 ∈ ( TermO ‘ 𝐸 ) )
15	1 13 14	termcterm2	⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( TermO ‘ 𝐸 ) ) → 𝐶 ∈ TermCat )
16	8 15	impbida	⊢ ( 𝜑 → ( 𝐶 ∈ TermCat ↔ 𝐶 ∈ ( TermO ‘ 𝐸 ) ) )