Theorem hashsnle1

Description: The size of a singleton is less than or equal to 1. (Contributed by AV, 23-Feb-2021)

	Ref	Expression
Assertion	hashsnle1	$$⊢\left|\left\{A\right\}\right|\le 1$$

Proof

Step	Hyp	Ref	Expression
1		hashsn01	$$⊢\left(\left|\left\{A\right\}\right|=0\vee \left|\left\{A\right\}\right|=1\right)$$
2		0le1	$$⊢0\le 1$$
3		breq1	$$⊢\left|\left\{A\right\}\right|=0\to \left(\left|\left\{A\right\}\right|\le 1\leftrightarrow 0\le 1\right)$$
4	2 3	mpbiri	$$⊢\left|\left\{A\right\}\right|=0\to \left|\left\{A\right\}\right|\le 1$$
5		1le1	$$⊢1\le 1$$
6		breq1	$$⊢\left|\left\{A\right\}\right|=1\to \left(\left|\left\{A\right\}\right|\le 1\leftrightarrow 1\le 1\right)$$
7	5 6	mpbiri	$$⊢\left|\left\{A\right\}\right|=1\to \left|\left\{A\right\}\right|\le 1$$
8	4 7	jaoi	$$⊢\left(\left|\left\{A\right\}\right|=0\vee \left|\left\{A\right\}\right|=1\right)\to \left|\left\{A\right\}\right|\le 1$$
9	1 8	ax-mp	$$⊢\left|\left\{A\right\}\right|\le 1$$