eufunclem

Description: If there exists a unique functor from a non-empty category, then the base of the target category is at most 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	eufunclem	$⊢ φ \to B ≼ 1_{𝑜}$

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		eqid	$⊢ D Δ_{func} C = D Δ_{func} C$
6		euex	$⊢ \exists! f f \in (C Func D) \to \exists f f \in (C Func D)$
7	1 6	syl	$⊢ φ \to \exists f f \in (C Func D)$
8		relfunc	$⊢ Rel (C Func D)$
9		1st2ndbr	$⊢ (Rel (C Func D) \land f \in (C Func D)) \to 1^{st} (f) (C Func D) 2^{nd} (f)$
10	8 9	mpan	$⊢ f \in (C Func D) \to 1^{st} (f) (C Func D) 2^{nd} (f)$
11	10	funcrcl3	$⊢ f \in (C Func D) \to D \in Cat$
12	11	exlimiv	$⊢ \exists f f \in (C Func D) \to D \in Cat$
13	7 12	syl	$⊢ φ \to D \in Cat$
14	10	funcrcl2	$⊢ f \in (C Func D) \to C \in Cat$
15	14	exlimiv	$⊢ \exists f f \in (C Func D) \to C \in Cat$
16	7 15	syl	$⊢ φ \to C \in Cat$
17	5 13 16 4 2 3	diag1f1	$⊢ φ \to 1^{st} (D Δ_{func} C) : B \underset{1-1}{⟶} C Func D$
18		ovex	$⊢ C Func D \in V$
19	18	f1dom	$⊢ 1^{st} (D Δ_{func} C) : B \underset{1-1}{⟶} C Func D \to B ≼ (C Func D)$
20	17 19	syl	$⊢ φ \to B ≼ (C Func D)$
21		euen1b	$⊢ (C Func D) \approx 1_{𝑜} \leftrightarrow \exists! f f \in (C Func D)$
22	1 21	sylibr	$⊢ φ \to (C Func D) \approx 1_{𝑜}$
23		domentr	$⊢ (B ≼ (C Func D) \land (C Func D) \approx 1_{𝑜}) \to B ≼ 1_{𝑜}$
24	20 22 23	syl2anc	$⊢ φ \to B ≼ 1_{𝑜}$

Metamath Proof Explorer

Theorem eufunclem

Proof