Metamath Proof Explorer


Theorem snct

Description: A singleton is countable. (Contributed by Thierry Arnoux, 16-Sep-2016)

Ref Expression
Assertion snct A V A ω

Proof

Step Hyp Ref Expression
1 ensn1g A V A 1 𝑜
2 peano1 ω
3 2 ne0ii ω
4 omex ω V
5 4 0sdom ω ω
6 3 5 mpbir ω
7 0sdom1dom ω 1 𝑜 ω
8 6 7 mpbi 1 𝑜 ω
9 endomtr A 1 𝑜 1 𝑜 ω A ω
10 1 8 9 sylancl A V A ω