This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )