Description: A singleton is countable. (Contributed by Thierry Arnoux, 16-Sep-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | snct |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ensn1g | ||
2 | peano1 | ||
3 | 2 | ne0ii | |
4 | omex | ||
5 | 4 | 0sdom | |
6 | 3 5 | mpbir | |
7 | 0sdom1dom | ||
8 | 6 7 | mpbi | |
9 | endomtr | ||
10 | 1 8 9 | sylancl |