This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to U \in V$
		termcterm3.c	$⊢ φ \to C \in U$
		termcterm3.1	$⊢ φ \to SetCat (1_{𝑜}) \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 = CatCat (U)$
2		termcterm3.u	$⊢ φ \to U \in V$
3		termcterm3.c	$⊢ φ \to C \in U$
4		termcterm3.1	$⊢ φ \to SetCat (1_{𝑜}) \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	$⊢ (φ \land C \in TermO (E)) \to C \in TermO (E)$
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 \|-