Theorem hash1snb

Description: The size of a set is 1 if and only if it is a singleton (containing a set). (Contributed by Alexander van der Vekens, 7-Dec-2017)

	Ref	Expression
Assertion	hash1snb	$$⊢V\in W\to \left(\left|V\right|=1\leftrightarrow \exists aV=\left\{a\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢\left|V\right|=1\to \left|V\right|=1$$
2		hash1	$$⊢\left|1_{𝑜}\right|=1$$
3	1 2	eqtr4di	$$⊢\left|V\right|=1\to \left|V\right|=\left|1_{𝑜}\right|$$
4	3	adantl	$$⊢\left(V\in \mathrm{Fin}\wedge \left|V\right|=1\right)\to \left|V\right|=\left|1_{𝑜}\right|$$
5		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
6		nnfi	$$⊢1_{𝑜}\in \mathrm{\omega }\to 1_{𝑜}\in \mathrm{Fin}$$
7	5 6	mp1i	$$⊢\left|V\right|=1\to 1_{𝑜}\in \mathrm{Fin}$$
8		hashen	$$⊢\left(V\in \mathrm{Fin}\wedge 1_{𝑜}\in \mathrm{Fin}\right)\to \left(\left|V\right|=\left|1_{𝑜}\right|\leftrightarrow V\approx 1_{𝑜}\right)$$
9	7 8	sylan2	$$⊢\left(V\in \mathrm{Fin}\wedge \left|V\right|=1\right)\to \left(\left|V\right|=\left|1_{𝑜}\right|\leftrightarrow V\approx 1_{𝑜}\right)$$
10	4 9	mpbid	$$⊢\left(V\in \mathrm{Fin}\wedge \left|V\right|=1\right)\to V\approx 1_{𝑜}$$
11		en1	$$⊢V\approx 1_{𝑜}\leftrightarrow \exists aV=\left\{a\right\}$$
12	10 11	sylib	$$⊢\left(V\in \mathrm{Fin}\wedge \left|V\right|=1\right)\to \exists aV=\left\{a\right\}$$
13	12	ex	$$⊢V\in \mathrm{Fin}\to \left(\left|V\right|=1\to \exists aV=\left\{a\right\}\right)$$
14	13	a1d	$$⊢V\in \mathrm{Fin}\to \left(V\in W\to \left(\left|V\right|=1\to \exists aV=\left\{a\right\}\right)\right)$$
15		hashinf	$$⊢\left(V\in W\wedge \neg V\in \mathrm{Fin}\right)\to \left|V\right|=\mathrm{+\infty }$$
16		eqeq1	$$⊢\left|V\right|=\mathrm{+\infty }\to \left(\left|V\right|=1\leftrightarrow \mathrm{+\infty }=1\right)$$
17		1re	$$⊢1\in ℝ$$
18		renepnf	$$⊢1\in ℝ\to 1\ne \mathrm{+\infty }$$
19		df-ne	$$⊢1\ne \mathrm{+\infty }\leftrightarrow \neg 1=\mathrm{+\infty }$$
20		pm2.21	$$⊢\neg 1=\mathrm{+\infty }\to \left(1=\mathrm{+\infty }\to \exists aV=\left\{a\right\}\right)$$
21	19 20	sylbi	$$⊢1\ne \mathrm{+\infty }\to \left(1=\mathrm{+\infty }\to \exists aV=\left\{a\right\}\right)$$
22	17 18 21	mp2b	$$⊢1=\mathrm{+\infty }\to \exists aV=\left\{a\right\}$$
23	22	eqcoms	$$⊢\mathrm{+\infty }=1\to \exists aV=\left\{a\right\}$$
24	16 23	syl6bi	$$⊢\left|V\right|=\mathrm{+\infty }\to \left(\left|V\right|=1\to \exists aV=\left\{a\right\}\right)$$
25	15 24	syl	$$⊢\left(V\in W\wedge \neg V\in \mathrm{Fin}\right)\to \left(\left|V\right|=1\to \exists aV=\left\{a\right\}\right)$$
26	25	expcom	$$⊢\neg V\in \mathrm{Fin}\to \left(V\in W\to \left(\left|V\right|=1\to \exists aV=\left\{a\right\}\right)\right)$$
27	14 26	pm2.61i	$$⊢V\in W\to \left(\left|V\right|=1\to \exists aV=\left\{a\right\}\right)$$
28		fveq2	$$⊢V=\left\{a\right\}\to \left|V\right|=\left|\left\{a\right\}\right|$$
29		hashsng	$$⊢a\in \mathrm{V}\to \left|\left\{a\right\}\right|=1$$
30	29	elv	$$⊢\left|\left\{a\right\}\right|=1$$
31	28 30	eqtrdi	$$⊢V=\left\{a\right\}\to \left|V\right|=1$$
32	31	exlimiv	$$⊢\exists aV=\left\{a\right\}\to \left|V\right|=1$$
33	27 32	impbid1	$$⊢V\in W\to \left(\left|V\right|=1\leftrightarrow \exists aV=\left\{a\right\}\right)$$