Theorem hashsn01

Description: The size of a singleton is either 0 or 1. (Contributed by AV, 23-Feb-2021)

	Ref	Expression
Assertion	hashsn01	$$⊢\left(\left|\left\{A\right\}\right|=0\vee \left|\left\{A\right\}\right|=1\right)$$

Proof

Step	Hyp	Ref	Expression
1		hashsng	$$⊢A\in \mathrm{V}\to \left|\left\{A\right\}\right|=1$$
2	1	olcd	$$⊢A\in \mathrm{V}\to \left(\left|\left\{A\right\}\right|=0\vee \left|\left\{A\right\}\right|=1\right)$$
3		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
4	3	biimpi	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}=\varnothing$$
5	4	fveq2d	$$⊢\neg A\in \mathrm{V}\to \left|\left\{A\right\}\right|=\left|\varnothing \right|$$
6		hash0	$$⊢\left|\varnothing \right|=0$$
7	5 6	eqtrdi	$$⊢\neg A\in \mathrm{V}\to \left|\left\{A\right\}\right|=0$$
8	7	orcd	$$⊢\neg A\in \mathrm{V}\to \left(\left|\left\{A\right\}\right|=0\vee \left|\left\{A\right\}\right|=1\right)$$
9	2 8	pm2.61i	$$⊢\left(\left|\left\{A\right\}\right|=0\vee \left|\left\{A\right\}\right|=1\right)$$