This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )