Theorem sn1dom

Description: A singleton is dominated by ordinal one. (Contributed by RP, 29-Oct-2023)

	Ref	Expression
Assertion	sn1dom	$$⊢\left\{A\right\}\preccurlyeq 1_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		ensn1g	$$⊢A\in \mathrm{V}\to \left\{A\right\}\approx 1_{𝑜}$$
2		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
3		domrefg	$$⊢1_{𝑜}\in \mathrm{On}\to 1_{𝑜}\preccurlyeq 1_{𝑜}$$
4	2 3	ax-mp	$$⊢1_{𝑜}\preccurlyeq 1_{𝑜}$$
5		endomtr	$$⊢\left(\left\{A\right\}\approx 1_{𝑜}\wedge 1_{𝑜}\preccurlyeq 1_{𝑜}\right)\to \left\{A\right\}\preccurlyeq 1_{𝑜}$$
6	1 4 5	sylancl	$$⊢A\in \mathrm{V}\to \left\{A\right\}\preccurlyeq 1_{𝑜}$$
7		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
8		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
9		eqeng	$$⊢\left\{A\right\}\in \mathrm{V}\to \left(\left\{A\right\}=\varnothing \to \left\{A\right\}\approx \varnothing \right)$$
10	8 9	ax-mp	$$⊢\left\{A\right\}=\varnothing \to \left\{A\right\}\approx \varnothing$$
11	7 10	sylbi	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}\approx \varnothing$$
12		0domg	$$⊢1_{𝑜}\in \mathrm{On}\to \varnothing \preccurlyeq 1_{𝑜}$$
13	2 12	ax-mp	$$⊢\varnothing \preccurlyeq 1_{𝑜}$$
14		endomtr	$$⊢\left(\left\{A\right\}\approx \varnothing \wedge \varnothing \preccurlyeq 1_{𝑜}\right)\to \left\{A\right\}\preccurlyeq 1_{𝑜}$$
15	11 13 14	sylancl	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}\preccurlyeq 1_{𝑜}$$
16	6 15	pm2.61i	$$⊢\left\{A\right\}\preccurlyeq 1_{𝑜}$$