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	|- ( ph -> C e. ThinCat )
	thincmo.x	|- ( ph -> X e. B )
	thincmo.y	|- ( ph -> Y e. B )
	thincn0eu.b	|- ( ph -> B = ( Base ` C ) )
	thincn0eu.h	|- ( ph -> H = ( Hom ` C ) )
Assertion	thincn0eu	|- ( ph -> ( ( X H Y ) =/= (/) <-> 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		thincn0eu.b	|- ( ph -> B = ( Base ` C ) )
5		thincn0eu.h	|- ( ph -> H = ( Hom ` C ) )
6		n0	|- ( ( X H Y ) =/= (/) <-> E. f f e. ( X H Y ) )
7	6	biimpi	|- ( ( X H Y ) =/= (/) -> E. f f e. ( X H Y ) )
8	1 2 3 4 5	thincmod	|- ( ph -> E* f f e. ( X H Y ) )
9	7 8	anim12i	|- ( ( ( X H Y ) =/= (/) /\ ph ) -> ( E. f f e. ( X H Y ) /\ E* f f e. ( X H Y ) ) )
10		df-eu	|- ( E! f f e. ( X H Y ) <-> ( E. f f e. ( X H Y ) /\ E* f f e. ( X H Y ) ) )
11	9 10	sylibr	|- ( ( ( X H Y ) =/= (/) /\ ph ) -> E! f f e. ( X H Y ) )
12	11	expcom	|- ( ph -> ( ( X H Y ) =/= (/) -> E! f f e. ( X H Y ) ) )
13		euex	|- ( E! f f e. ( X H Y ) -> E. f f e. ( X H Y ) )
14	13 6	sylibr	|- ( E! f f e. ( X H Y ) -> ( X H Y ) =/= (/) )
15	12 14	impbid1	|- ( ph -> ( ( X H Y ) =/= (/) <-> E! f f e. ( X H Y ) ) )