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 
|- ( ( 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 ) )