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	|- ( ( C Func C ) ~~ 1o -> ( ( Base ` C ) = (/) \/ C e. TermCat ) )

Proof

Step	Hyp	Ref	Expression
1		euen1b	|- ( ( C Func C ) ~~ 1o <-> E! f f e. ( C Func C ) )
2	1	biimpi	|- ( ( C Func C ) ~~ 1o -> E! f f e. ( C Func C ) )
3	2	adantr	|- ( ( ( C Func C ) ~~ 1o /\ -. ( Base ` C ) = (/) ) -> E! f f e. ( C Func C ) )
4		eqid	|- ( Base ` C ) = ( Base ` C )
5		simpr	|- ( ( ( C Func C ) ~~ 1o /\ -. ( Base ` C ) = (/) ) -> -. ( Base ` C ) = (/) )
6	5	neqned	|- ( ( ( C Func C ) ~~ 1o /\ -. ( Base ` C ) = (/) ) -> ( Base ` C ) =/= (/) )
7	3 4 6	euendfunc	|- ( ( ( C Func C ) ~~ 1o /\ -. ( Base ` C ) = (/) ) -> C e. TermCat )
8	7	ex	|- ( ( C Func C ) ~~ 1o -> ( -. ( Base ` C ) = (/) -> C e. TermCat ) )
9	8	orrd	|- ( ( C Func C ) ~~ 1o -> ( ( Base ` C ) = (/) \/ C e. TermCat ) )