thincmo

Description: There is at most one morphism in each hom-set. (Contributed by Zhi Wang, 21-Sep-2024)

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		thincmo.b	$⊢ B = {Base}_{C}$
5		thincmo.h	$⊢ H = Hom (C)$
6	2	adantr	$⊢ (φ \land (f \in (X H Y) \land g \in (X H Y))) \to X \in B$
7	3	adantr	$⊢ (φ \land (f \in (X H Y) \land g \in (X H Y))) \to Y \in B$
8		simprl	$⊢ (φ \land (f \in (X H Y) \land g \in (X H Y))) \to f \in (X H Y)$
9		simprr	$⊢ (φ \land (f \in (X H Y) \land g \in (X H Y))) \to g \in (X H Y)$
10	1	adantr	$⊢ (φ \land (f \in (X H Y) \land g \in (X H Y))) \to C \in ThinCat$
11	6 7 8 9 4 5 10	thincmo2	$⊢ (φ \land (f \in (X H Y) \land g \in (X H Y))) \to f = g$
12	11	ex	$⊢ φ \to ((f \in (X H Y) \land g \in (X H Y)) \to f = g)$
13	12	alrimivv	$⊢ φ \to \forall f \forall g ((f \in (X H Y) \land g \in (X H Y)) \to f = g)$
14		eleq1w	$⊢ f = g \to (f \in (X H Y) \leftrightarrow g \in (X H Y))$
15	14	mo4	$⊢ \exists^{*} f f \in (X H Y) \leftrightarrow \forall f \forall g ((f \in (X H Y) \land g \in (X H Y)) \to f = g)$
16	13 15	sylibr	$⊢ φ \to \exists^{*} f f \in (X H Y)$

Metamath Proof Explorer