Theorem 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	⊢ ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
	eufunc.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	eufunc.0	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
	eufunc.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
Assertion	eufunclem	⊢ ( 𝜑 → 𝐵 ≼ 1o )

Proof

Step	Hyp	Ref	Expression
1		eufunc.f	⊢ ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
2		eufunc.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
3		eufunc.0	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
4		eufunc.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
5		eqid	⊢ ( 𝐷 Δfunc 𝐶 ) = ( 𝐷 Δfunc 𝐶 )
6		euex	⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) → ∃ 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
7	1 6	syl	⊢ ( 𝜑 → ∃ 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
8		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
9		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1st ‘ 𝑓 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝑓 ) )
10	8 9	mpan	⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) → ( 1st ‘ 𝑓 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝑓 ) )
11	10	funcrcl3	⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) → 𝐷 ∈ Cat )
12	11	exlimiv	⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) → 𝐷 ∈ Cat )
13	7 12	syl	⊢ ( 𝜑 → 𝐷 ∈ Cat )
14	10	funcrcl2	⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) → 𝐶 ∈ Cat )
15	14	exlimiv	⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) → 𝐶 ∈ Cat )
16	7 15	syl	⊢ ( 𝜑 → 𝐶 ∈ Cat )
17	5 13 16 4 2 3	diag1f1	⊢ ( 𝜑 → ( 1st ‘ ( 𝐷 Δfunc 𝐶 ) ) : 𝐵 –1-1→ ( 𝐶 Func 𝐷 ) )
18		ovex	⊢ ( 𝐶 Func 𝐷 ) ∈ V
19	18	f1dom	⊢ ( ( 1st ‘ ( 𝐷 Δfunc 𝐶 ) ) : 𝐵 –1-1→ ( 𝐶 Func 𝐷 ) → 𝐵 ≼ ( 𝐶 Func 𝐷 ) )
20	17 19	syl	⊢ ( 𝜑 → 𝐵 ≼ ( 𝐶 Func 𝐷 ) )
21		euen1b	⊢ ( ( 𝐶 Func 𝐷 ) ≈ 1o ↔ ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
22	1 21	sylibr	⊢ ( 𝜑 → ( 𝐶 Func 𝐷 ) ≈ 1o )
23		domentr	⊢ ( ( 𝐵 ≼ ( 𝐶 Func 𝐷 ) ∧ ( 𝐶 Func 𝐷 ) ≈ 1o ) → 𝐵 ≼ 1o )
24	20 22 23	syl2anc	⊢ ( 𝜑 → 𝐵 ≼ 1o )