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	⊢ ( 𝜑 → ( ( 𝑋 𝐻 𝑌 ) ≠ ∅ ↔ ∃! 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) )