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

Metamath Proof Explorer

Theorem euendfunc2

Description: If there exists a unique endofunctor (a functor from a category to itself) for a category, then it is either initial (empty) or terminal. (Contributed by Zhi Wang, 20-Oct-2025)

		Ref	Expression
	Assertion	euendfunc2	Could not format assertion : No typesetting found for \|- ( ( C Func C ) ~~ 1o -> ( ( Base ` C ) = (/) \/ C e. TermCat ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		euen1b	$⊢ (C Func C) \approx 1_{𝑜} \leftrightarrow \exists! f f \in (C Func C)$
2	1	biimpi	$⊢ (C Func C) \approx 1_{𝑜} \to \exists! f f \in (C Func C)$
3	2	adantr	$⊢ ((C Func C) \approx 1_{𝑜} \land \neg {Base}_{C} = \emptyset) \to \exists! f f \in (C Func C)$
4		eqid	$⊢ {Base}_{C} = {Base}_{C}$
5		simpr	$⊢ ((C Func C) \approx 1_{𝑜} \land \neg {Base}_{C} = \emptyset) \to \neg {Base}_{C} = \emptyset$
6	5	neqned	$⊢ ((C Func C) \approx 1_{𝑜} \land \neg {Base}_{C} = \emptyset) \to {Base}_{C} \neq \emptyset$
7	3 4 6	euendfunc	Could not format ( ( ( C Func C ) ~~ 1o /\ -. ( Base ` C ) = (/) ) -> C e. TermCat ) : No typesetting found for \|- ( ( ( C Func C ) ~~ 1o /\ -. ( Base ` C ) = (/) ) -> C e. TermCat ) with typecode \|-
8	7	ex	Could not format ( ( C Func C ) ~~ 1o -> ( -. ( Base ` C ) = (/) -> C e. TermCat ) ) : No typesetting found for \|- ( ( C Func C ) ~~ 1o -> ( -. ( Base ` C ) = (/) -> C e. TermCat ) ) with typecode \|-
9	8	orrd	Could not format ( ( C Func C ) ~~ 1o -> ( ( Base ` C ) = (/) \/ C e. TermCat ) ) : No typesetting found for \|- ( ( C Func C ) ~~ 1o -> ( ( Base ` C ) = (/) \/ C e. TermCat ) ) with typecode \|-