Theorem eufunc

Description: If there exists a unique functor from a non-empty category, then the base of the target category is a singleton. (Contributed by Zhi Wang, 19-Oct-2025)

	Ref	Expression
Hypotheses	eufunc.f	⊢ ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
	eufunc.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	eufunc.0	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
	eufunc.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
Assertion	eufunc	⊢ ( 𝜑 → ∃! 𝑥 𝑥 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eufunc.f	⊢ ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
2		eufunc.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
3		eufunc.0	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
4		eufunc.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
5		euex	⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) → ∃ 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
6		simpr	⊢ ( ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐵 = ∅ ) → 𝐵 = ∅ )
7		simpl	⊢ ( ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐵 = ∅ ) → 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
8	2 4 6 7	func0g2	⊢ ( ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐵 = ∅ ) → 𝐴 = ∅ )
9	8	ex	⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐵 = ∅ → 𝐴 = ∅ ) )
10	9	exlimiv	⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐵 = ∅ → 𝐴 = ∅ ) )
11	1 5 10	3syl	⊢ ( 𝜑 → ( 𝐵 = ∅ → 𝐴 = ∅ ) )
12	11	imp	⊢ ( ( 𝜑 ∧ 𝐵 = ∅ ) → 𝐴 = ∅ )
13	3 12	mteqand	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
14		n0	⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐵 )
15	13 14	sylib	⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ 𝐵 )
16	1 2 3 4	eufunclem	⊢ ( 𝜑 → 𝐵 ≼ 1o )
17		modom2	⊢ ( ∃* 𝑥 𝑥 ∈ 𝐵 ↔ 𝐵 ≼ 1o )
18	16 17	sylibr	⊢ ( 𝜑 → ∃* 𝑥 𝑥 ∈ 𝐵 )
19		df-eu	⊢ ( ∃! 𝑥 𝑥 ∈ 𝐵 ↔ ( ∃ 𝑥 𝑥 ∈ 𝐵 ∧ ∃* 𝑥 𝑥 ∈ 𝐵 ) )
20	15 18 19	sylanbrc	⊢ ( 𝜑 → ∃! 𝑥 𝑥 ∈ 𝐵 )