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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 eufunc.f ⊢ ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
2 eufunc.a ⊢ 𝐴 = ( Base ‘ 𝐶 )
3 eufunc.0 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
4 eufunc.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
5 euex ⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) → ∃ 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
6 simpr ⊢ ( ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐵 = ∅ ) → 𝐵 = ∅ )
7 simpl ⊢ ( ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐵 = ∅ ) → 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
8 2 4 6 7 func0g2 ⊢ ( ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐵 = ∅ ) → 𝐴 = ∅ )
9 8 ex ⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐵 = ∅ → 𝐴 = ∅ ) )
10 9 exlimiv ⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐵 = ∅ → 𝐴 = ∅ ) )
11 1 5 10 3syl ⊢ ( 𝜑 → ( 𝐵 = ∅ → 𝐴 = ∅ ) )
12 11 imp ⊢ ( ( 𝜑 ∧ 𝐵 = ∅ ) → 𝐴 = ∅ )
13 3 12 mteqand ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
14 n0 ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐵 )
15 13 14 sylib ⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ 𝐵 )
16 1 2 3 4 eufunclem ⊢ ( 𝜑 → 𝐵 ≼ 1o )
17 modom2 ⊢ ( ∃* 𝑥 𝑥 ∈ 𝐵 ↔ 𝐵 ≼ 1o )
18 16 17 sylibr ⊢ ( 𝜑 → ∃* 𝑥 𝑥 ∈ 𝐵 )
19 df-eu ⊢ ( ∃! 𝑥 𝑥 ∈ 𝐵 ↔ ( ∃ 𝑥 𝑥 ∈ 𝐵 ∧ ∃* 𝑥 𝑥 ∈ 𝐵 ) )
20 15 18 19 sylanbrc ⊢ ( 𝜑 → ∃! 𝑥 𝑥 ∈ 𝐵 )