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	$⊢ φ \to C \in ThinCat$
	thincmo.x	$⊢ φ \to X \in B$
	thincmo.y	$⊢ φ \to Y \in B$
	thincn0eu.b	$⊢ φ \to B = {Base}_{C}$
	thincn0eu.h	$⊢ φ \to H = Hom (C)$
Assertion	thincn0eu	$⊢ φ \to (X H Y \neq \emptyset \leftrightarrow \exists! f f \in (X H Y))$

Step	Hyp	Ref	Expression
1		thincmo.c	$⊢ φ \to C \in ThinCat$
2		thincmo.x	$⊢ φ \to X \in B$
3		thincmo.y	$⊢ φ \to Y \in B$
4		thincn0eu.b	$⊢ φ \to B = {Base}_{C}$
5		thincn0eu.h	$⊢ φ \to H = Hom (C)$
6		n0	$⊢ X H Y \neq \emptyset \leftrightarrow \exists f f \in (X H Y)$
7	6	biimpi	$⊢ X H Y \neq \emptyset \to \exists f f \in (X H Y)$
8	1 2 3 4 5	thincmod	$⊢ φ \to \exists^{*} f f \in (X H Y)$
9	7 8	anim12i	$⊢ (X H Y \neq \emptyset \land φ) \to (\exists f f \in (X H Y) \land \exists^{*} f f \in (X H Y))$
10		df-eu	$⊢ \exists! f f \in (X H Y) \leftrightarrow (\exists f f \in (X H Y) \land \exists^{*} f f \in (X H Y))$
11	9 10	sylibr	$⊢ (X H Y \neq \emptyset \land φ) \to \exists! f f \in (X H Y)$
12	11	expcom	$⊢ φ \to (X H Y \neq \emptyset \to \exists! f f \in (X H Y))$
13		euex	$⊢ \exists! f f \in (X H Y) \to \exists f f \in (X H Y)$
14	13 6	sylibr	$⊢ \exists! f f \in (X H Y) \to X H Y \neq \emptyset$
15	12 14	impbid1	$⊢ φ \to (X H Y \neq \emptyset \leftrightarrow \exists! f f \in (X H Y))$

Metamath Proof Explorer