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=\mathrm{CatCat}\left(U\right)$$
	termcterm3.u	$$⊢\phi \to U\in V$$
	termcterm3.c	$$⊢\phi \to C\in U$$
	termcterm3.1	$$⊢\phi \to \mathrm{SetCat}\left(1_{𝑜}\right)\in U$$
Assertion	termcterm3	Could not format assertion : No typesetting found for |- ( ph -> ( C e. TermCat <-> C e. ( TermO ` E ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		termcterm.e	$$⊢E=\mathrm{CatCat}\left(U\right)$$
2		termcterm3.u	$$⊢\phi \to U\in V$$
3		termcterm3.c	$$⊢\phi \to C\in U$$
4		termcterm3.1	$$⊢\phi \to \mathrm{SetCat}\left(1_{𝑜}\right)\in U$$
5	2	adantr	Could not format ( ( ph /\ C e. TermCat ) -> U e. V ) : No typesetting found for |- ( ( ph /\ C e. TermCat ) -> U e. V ) with typecode |-
6	3	adantr	Could not format ( ( ph /\ C e. TermCat ) -> C e. U ) : No typesetting found for |- ( ( ph /\ C e. TermCat ) -> C e. U ) with typecode |-
7		simpr	Could not format ( ( ph /\ C e. TermCat ) -> C e. TermCat ) : No typesetting found for |- ( ( ph /\ C e. TermCat ) -> C e. TermCat ) with typecode |-
8	1 5 6 7	termcterm	Could not format ( ( ph /\ C e. TermCat ) -> C e. ( TermO ` E ) ) : No typesetting found for |- ( ( ph /\ C e. TermCat ) -> C e. ( TermO ` E ) ) with typecode |-
9		setc1oterm	Could not format ( SetCat ` 1o ) e. TermCat : No typesetting found for |- ( SetCat ` 1o ) e. TermCat with typecode |-
10	9	a1i	Could not format ( ph -> ( SetCat ` 1o ) e. TermCat ) : No typesetting found for |- ( ph -> ( SetCat ` 1o ) e. TermCat ) with typecode |-
11	4 10	elind	Could not format ( ph -> ( SetCat ` 1o ) e. ( U i^i TermCat ) ) : No typesetting found for |- ( ph -> ( SetCat ` 1o ) e. ( U i^i TermCat ) ) with typecode |-
12	11	ne0d	Could not format ( ph -> ( U i^i TermCat ) =/= (/) ) : No typesetting found for |- ( ph -> ( U i^i TermCat ) =/= (/) ) with typecode |-
13	12	adantr	Could not format ( ( ph /\ C e. ( TermO ` E ) ) -> ( U i^i TermCat ) =/= (/) ) : No typesetting found for |- ( ( ph /\ C e. ( TermO ` E ) ) -> ( U i^i TermCat ) =/= (/) ) with typecode |-
14		simpr	$$⊢\left(\phi \wedge C\in \mathrm{TermO}\left(E\right)\right)\to C\in \mathrm{TermO}\left(E\right)$$
15	1 13 14	termcterm2	Could not format ( ( ph /\ C e. ( TermO ` E ) ) -> C e. TermCat ) : No typesetting found for |- ( ( ph /\ C e. ( TermO ` E ) ) -> C e. TermCat ) with typecode |-
16	8 15	impbida	Could not format ( ph -> ( C e. TermCat <-> C e. ( TermO ` E ) ) ) : No typesetting found for |- ( ph -> ( C e. TermCat <-> C e. ( TermO ` E ) ) ) with typecode |-