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	$⊢ φ \to \exists! f f \in (C Func D)$
	eufunc.a	$⊢ A = {Base}_{C}$
	eufunc.0	$⊢ φ \to A \neq \emptyset$
	eufunc.b	$⊢ B = {Base}_{D}$
Assertion	eufunc	$⊢ φ \to \exists! x x \in B$

Proof

Step	Hyp	Ref	Expression
1		eufunc.f	$⊢ φ \to \exists! f f \in (C Func D)$
2		eufunc.a	$⊢ A = {Base}_{C}$
3		eufunc.0	$⊢ φ \to A \neq \emptyset$
4		eufunc.b	$⊢ B = {Base}_{D}$
5		euex	$⊢ \exists! f f \in (C Func D) \to \exists f f \in (C Func D)$
6		simpr	$⊢ (f \in (C Func D) \land B = \emptyset) \to B = \emptyset$
7		simpl	$⊢ (f \in (C Func D) \land B = \emptyset) \to f \in (C Func D)$
8	2 4 6 7	func0g2	$⊢ (f \in (C Func D) \land B = \emptyset) \to A = \emptyset$
9	8	ex	$⊢ f \in (C Func D) \to (B = \emptyset \to A = \emptyset)$
10	9	exlimiv	$⊢ \exists f f \in (C Func D) \to (B = \emptyset \to A = \emptyset)$
11	1 5 10	3syl	$⊢ φ \to (B = \emptyset \to A = \emptyset)$
12	11	imp	$⊢ (φ \land B = \emptyset) \to A = \emptyset$
13	3 12	mteqand	$⊢ φ \to B \neq \emptyset$
14		n0	$⊢ B \neq \emptyset \leftrightarrow \exists x x \in B$
15	13 14	sylib	$⊢ φ \to \exists x x \in B$
16	1 2 3 4	eufunclem	$⊢ φ \to B ≼ 1_{𝑜}$
17		modom2	$⊢ \exists^{*} x x \in B \leftrightarrow B ≼ 1_{𝑜}$
18	16 17	sylibr	$⊢ φ \to \exists^{*} x x \in B$
19		df-eu	$⊢ \exists! x x \in B \leftrightarrow (\exists x x \in B \land \exists^{*} x x \in B)$
20	15 18 19	sylanbrc	$⊢ φ \to \exists! x x \in B$

Metamath Proof Explorer

Theorem eufunc

Proof