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	|- E = ( CatCat ` U )
	termcterm3.u	|- ( ph -> U e. V )
	termcterm3.c	|- ( ph -> C e. U )
	termcterm3.1	|- ( ph -> ( SetCat ` 1o ) e. U )
Assertion	termcterm3	|- ( ph -> ( C e. TermCat <-> C e. ( TermO ` E ) ) )

Proof

Step	Hyp	Ref	Expression
1		termcterm.e	|- E = ( CatCat ` U )
2		termcterm3.u	|- ( ph -> U e. V )
3		termcterm3.c	|- ( ph -> C e. U )
4		termcterm3.1	|- ( ph -> ( SetCat ` 1o ) e. U )
5	2	adantr	|- ( ( ph /\ C e. TermCat ) -> U e. V )
6	3	adantr	|- ( ( ph /\ C e. TermCat ) -> C e. U )
7		simpr	|- ( ( ph /\ C e. TermCat ) -> C e. TermCat )
8	1 5 6 7	termcterm	|- ( ( ph /\ C e. TermCat ) -> C e. ( TermO ` E ) )
9		setc1oterm	|- ( SetCat ` 1o ) e. TermCat
10	9	a1i	|- ( ph -> ( SetCat ` 1o ) e. TermCat )
11	4 10	elind	|- ( ph -> ( SetCat ` 1o ) e. ( U i^i TermCat ) )
12	11	ne0d	|- ( ph -> ( U i^i TermCat ) =/= (/) )
13	12	adantr	|- ( ( ph /\ C e. ( TermO ` E ) ) -> ( U i^i TermCat ) =/= (/) )
14		simpr	|- ( ( ph /\ C e. ( TermO ` E ) ) -> C e. ( TermO ` E ) )
15	1 13 14	termcterm2	|- ( ( ph /\ C e. ( TermO ` E ) ) -> C e. TermCat )
16	8 15	impbida	|- ( ph -> ( C e. TermCat <-> C e. ( TermO ` E ) ) )