Description: A category of sets all of whose objects contain at most one element is thin. (Contributed by Zhi Wang, 20-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | setcthin.c | |
|
setcthin.u | |
||
setcthin.x | |
||
Assertion | setcthin | Could not format assertion : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |- |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | setcthin.c | |
|
2 | setcthin.u | |
|
3 | setcthin.x | |
|
4 | eqid | |
|
5 | 4 2 | setcbas | |
6 | eqidd | |
|
7 | elequ2 | |
|
8 | 7 | mobidv | |
9 | 3 | adantr | |
10 | simprr | |
|
11 | 8 9 10 | rspcdva | |
12 | mofmo | |
|
13 | 11 12 | syl | |
14 | 2 | adantr | |
15 | eqid | |
|
16 | simprl | |
|
17 | 4 14 15 16 10 | elsetchom | |
18 | 17 | mobidv | |
19 | 13 18 | mpbird | |
20 | 4 | setccat | |
21 | 2 20 | syl | |
22 | 5 6 19 21 | isthincd | Could not format ( ph -> ( SetCat ` U ) e. ThinCat ) : No typesetting found for |- ( ph -> ( SetCat ` U ) e. ThinCat ) with typecode |- |
23 | 1 22 | eqeltrd | Could not format ( ph -> C e. ThinCat ) : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |- |