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	⊢ ( ( 𝐶 Func 𝐶 ) ≈ 1o → ( ( Base ‘ 𝐶 ) = ∅ ∨ 𝐶 ∈ TermCat ) )

Proof

Step	Hyp	Ref	Expression
1		euen1b	⊢ ( ( 𝐶 Func 𝐶 ) ≈ 1o ↔ ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐶 ) )
2	1	biimpi	⊢ ( ( 𝐶 Func 𝐶 ) ≈ 1o → ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐶 ) )
3	2	adantr	⊢ ( ( ( 𝐶 Func 𝐶 ) ≈ 1o ∧ ¬ ( Base ‘ 𝐶 ) = ∅ ) → ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐶 ) )
4		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5		simpr	⊢ ( ( ( 𝐶 Func 𝐶 ) ≈ 1o ∧ ¬ ( Base ‘ 𝐶 ) = ∅ ) → ¬ ( Base ‘ 𝐶 ) = ∅ )
6	5	neqned	⊢ ( ( ( 𝐶 Func 𝐶 ) ≈ 1o ∧ ¬ ( Base ‘ 𝐶 ) = ∅ ) → ( Base ‘ 𝐶 ) ≠ ∅ )
7	3 4 6	euendfunc	⊢ ( ( ( 𝐶 Func 𝐶 ) ≈ 1o ∧ ¬ ( Base ‘ 𝐶 ) = ∅ ) → 𝐶 ∈ TermCat )
8	7	ex	⊢ ( ( 𝐶 Func 𝐶 ) ≈ 1o → ( ¬ ( Base ‘ 𝐶 ) = ∅ → 𝐶 ∈ TermCat ) )
9	8	orrd	⊢ ( ( 𝐶 Func 𝐶 ) ≈ 1o → ( ( Base ‘ 𝐶 ) = ∅ ∨ 𝐶 ∈ TermCat ) )