Theorem thincmo

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

	Ref	Expression
Hypotheses	thincmo.c	|- ( ph -> C e. ThinCat )
	thincmo.x	|- ( ph -> X e. B )
	thincmo.y	|- ( ph -> Y e. B )
	thincmo.b	|- B = ( Base ` C )
	thincmo.h	|- H = ( Hom ` C )
Assertion	thincmo	|- ( ph -> E* f f e. ( X H Y ) )

Proof

Step	Hyp	Ref	Expression
1		thincmo.c	|- ( ph -> C e. ThinCat )
2		thincmo.x	|- ( ph -> X e. B )
3		thincmo.y	|- ( ph -> Y e. B )
4		thincmo.b	|- B = ( Base ` C )
5		thincmo.h	|- H = ( Hom ` C )
6	2	adantr	|- ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> X e. B )
7	3	adantr	|- ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> Y e. B )
8		simprl	|- ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> f e. ( X H Y ) )
9		simprr	|- ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> g e. ( X H Y ) )
10	1	adantr	|- ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> C e. ThinCat )
11	6 7 8 9 4 5 10	thincmo2	|- ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> f = g )
12	11	ex	|- ( ph -> ( ( f e. ( X H Y ) /\ g e. ( X H Y ) ) -> f = g ) )
13	12	alrimivv	|- ( ph -> A. f A. g ( ( f e. ( X H Y ) /\ g e. ( X H Y ) ) -> f = g ) )
14		eleq1w	|- ( f = g -> ( f e. ( X H Y ) <-> g e. ( X H Y ) ) )
15	14	mo4	|- ( E* f f e. ( X H Y ) <-> A. f A. g ( ( f e. ( X H Y ) /\ g e. ( X H Y ) ) -> f = g ) )
16	13 15	sylibr	|- ( ph -> E* f f e. ( X H Y ) )