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 | |
||
thincmo.y | |
||
thincn0eu.b | |
||
thincn0eu.h | |
||
Assertion | thincn0eu | |
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 | |
|
3 | thincmo.y | |
|
4 | thincn0eu.b | |
|
5 | thincn0eu.h | |
|
6 | n0 | |
|
7 | 6 | biimpi | |
8 | 1 2 3 4 5 | thincmod | |
9 | 7 8 | anim12i | |
10 | df-eu | |
|
11 | 9 10 | sylibr | |
12 | 11 | expcom | |
13 | euex | |
|
14 | 13 6 | sylibr | |
15 | 12 14 | impbid1 | |