Theorem prhash2ex

Description: There is (at least) one set with two different elements: the unordered pair containing 0 and 1 . In contrast to pr0hash2ex , numbers are used instead of sets because their representation is shorter (and more comprehensive). (Contributed by AV, 29-Jan-2020)

	Ref	Expression
Assertion	prhash2ex	$$⊢\left|\left\{0,1\right\}\right|=2$$

Proof

Step	Hyp	Ref	Expression
1		0ne1	$$⊢0\ne 1$$
2		c0ex	$$⊢0\in \mathrm{V}$$
3		1ex	$$⊢1\in \mathrm{V}$$
4		hashprg	$$⊢\left(0\in \mathrm{V}\wedge 1\in \mathrm{V}\right)\to \left(0\ne 1\leftrightarrow \left|\left\{0,1\right\}\right|=2\right)$$
5	4	bicomd	$$⊢\left(0\in \mathrm{V}\wedge 1\in \mathrm{V}\right)\to \left(\left|\left\{0,1\right\}\right|=2\leftrightarrow 0\ne 1\right)$$
6	2 3 5	mp2an	$$⊢\left|\left\{0,1\right\}\right|=2\leftrightarrow 0\ne 1$$
7	1 6	mpbir	$$⊢\left|\left\{0,1\right\}\right|=2$$