Theorem snct

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

	Ref	Expression
Assertion	snct	$$⊢A\in V\to \left\{A\right\}\preccurlyeq \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		ensn1g	$$⊢A\in V\to \left\{A\right\}\approx 1_{𝑜}$$
2		peano1	$$⊢\varnothing \in \mathrm{\omega }$$
3	2	ne0ii	$$⊢\mathrm{\omega }\ne \varnothing$$
4		omex	$$⊢\mathrm{\omega }\in \mathrm{V}$$
5	4	0sdom	$$⊢\varnothing \prec \mathrm{\omega }\leftrightarrow \mathrm{\omega }\ne \varnothing$$
6	3 5	mpbir	$$⊢\varnothing \prec \mathrm{\omega }$$
7		0sdom1dom	$$⊢\varnothing \prec \mathrm{\omega }\leftrightarrow 1_{𝑜}\preccurlyeq \mathrm{\omega }$$
8	6 7	mpbi	$$⊢1_{𝑜}\preccurlyeq \mathrm{\omega }$$
9		endomtr	$$⊢\left(\left\{A\right\}\approx 1_{𝑜}\wedge 1_{𝑜}\preccurlyeq \mathrm{\omega }\right)\to \left\{A\right\}\preccurlyeq \mathrm{\omega }$$
10	1 8 9	sylancl	$$⊢A\in V\to \left\{A\right\}\preccurlyeq \mathrm{\omega }$$