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

Metamath Proof Explorer

Theorem thincn0eu

Description: In a thin category, a hom-set being non-empty is equivalent to having a unique element. (Contributed by Zhi Wang, 21-Sep-2024)

Ref Expression
Hypotheses thincmo.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
thincmo.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
thincmo.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
thincn0eu.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
thincn0eu.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
Assertion thincn0eu ( 𝜑 → ( ( 𝑋 𝐻 𝑌 ) ≠ ∅ ↔ ∃! 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 thincmo.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
2 thincmo.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
3 thincmo.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
4 thincn0eu.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
5 thincn0eu.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
6 n0 ⊢ ( ( 𝑋 𝐻 𝑌 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
7 6 biimpi ⊢ ( ( 𝑋 𝐻 𝑌 ) ≠ ∅ → ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
8 1 2 3 4 5 thincmod ⊢ ( 𝜑 → ∃* 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
9 7 8 anim12i ⊢ ( ( ( 𝑋 𝐻 𝑌 ) ≠ ∅ ∧ 𝜑 ) → ( ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∃* 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) )
10 df-eu ⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↔ ( ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∃* 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) )
11 9 10 sylibr ⊢ ( ( ( 𝑋 𝐻 𝑌 ) ≠ ∅ ∧ 𝜑 ) → ∃! 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
12 11 expcom ⊢ ( 𝜑 → ( ( 𝑋 𝐻 𝑌 ) ≠ ∅ → ∃! 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) )
13 euex ⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) → ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
14 13 6 sylibr ⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) → ( 𝑋 𝐻 𝑌 ) ≠ ∅ )
15 12 14 impbid1 ⊢ ( 𝜑 → ( ( 𝑋 𝐻 𝑌 ) ≠ ∅ ↔ ∃! 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) )