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	|- ( ph -> E! f f e. ( C Func D ) )
	eufunc.a	|- A = ( Base ` C )
	eufunc.0	|- ( ph -> A =/= (/) )
	eufunc.b	|- B = ( Base ` D )
Assertion	eufunc	|- ( ph -> E! x x e. B )

Proof

Step	Hyp	Ref	Expression
1		eufunc.f	|- ( ph -> E! f f e. ( C Func D ) )
2		eufunc.a	|- A = ( Base ` C )
3		eufunc.0	|- ( ph -> A =/= (/) )
4		eufunc.b	|- B = ( Base ` D )
5		euex	|- ( E! f f e. ( C Func D ) -> E. f f e. ( C Func D ) )
6		simpr	|- ( ( f e. ( C Func D ) /\ B = (/) ) -> B = (/) )
7		simpl	|- ( ( f e. ( C Func D ) /\ B = (/) ) -> f e. ( C Func D ) )
8	2 4 6 7	func0g2	|- ( ( f e. ( C Func D ) /\ B = (/) ) -> A = (/) )
9	8	ex	|- ( f e. ( C Func D ) -> ( B = (/) -> A = (/) ) )
10	9	exlimiv	|- ( E. f f e. ( C Func D ) -> ( B = (/) -> A = (/) ) )
11	1 5 10	3syl	|- ( ph -> ( B = (/) -> A = (/) ) )
12	11	imp	|- ( ( ph /\ B = (/) ) -> A = (/) )
13	3 12	mteqand	|- ( ph -> B =/= (/) )
14		n0	|- ( B =/= (/) <-> E. x x e. B )
15	13 14	sylib	|- ( ph -> E. x x e. B )
16	1 2 3 4	eufunclem	|- ( ph -> B ~<_ 1o )
17		modom2	|- ( E* x x e. B <-> B ~<_ 1o )
18	16 17	sylibr	|- ( ph -> E* x x e. B )
19		df-eu	|- ( E! x x e. B <-> ( E. x x e. B /\ E* x x e. B ) )
20	15 18 19	sylanbrc	|- ( ph -> E! x x e. B )