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 No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
thincmo.x φXB
thincmo.y φYB
thincn0eu.b φB=BaseC
thincn0eu.h φH=HomC
Assertion thincn0eu φXHY∃!ffXHY

Proof

Step Hyp Ref Expression
1 thincmo.c Could not format ( ph -> C e. ThinCat ) : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
2 thincmo.x φXB
3 thincmo.y φYB
4 thincn0eu.b φB=BaseC
5 thincn0eu.h φH=HomC
6 n0 XHYffXHY
7 6 biimpi XHYffXHY
8 1 2 3 4 5 thincmod φ*ffXHY
9 7 8 anim12i XHYφffXHY*ffXHY
10 df-eu ∃!ffXHYffXHY*ffXHY
11 9 10 sylibr XHYφ∃!ffXHY
12 11 expcom φXHY∃!ffXHY
13 euex ∃!ffXHYffXHY
14 13 6 sylibr ∃!ffXHYXHY
15 12 14 impbid1 φXHY∃!ffXHY