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	$$⊢\left(C\mathrm{Func}C\right)\approx 1_{𝑜}\leftrightarrow \exists !ff\in \left(C\mathrm{Func}C\right)$$
2	1	biimpi	$$⊢\left(C\mathrm{Func}C\right)\approx 1_{𝑜}\to \exists !ff\in \left(C\mathrm{Func}C\right)$$
3	2	adantr	$$⊢\left(\left(C\mathrm{Func}C\right)\approx 1_{𝑜}\wedge \neg {\mathrm{Base}}_C=\varnothing \right)\to \exists !ff\in \left(C\mathrm{Func}C\right)$$
4		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
5		simpr	$$⊢\left(\left(C\mathrm{Func}C\right)\approx 1_{𝑜}\wedge \neg {\mathrm{Base}}_C=\varnothing \right)\to \neg {\mathrm{Base}}_C=\varnothing$$
6	5	neqned	$$⊢\left(\left(C\mathrm{Func}C\right)\approx 1_{𝑜}\wedge \neg {\mathrm{Base}}_C=\varnothing \right)\to {\mathrm{Base}}_C\ne \varnothing$$
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 |-