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