Theorem hashsng

Description: The size of a singleton. (Contributed by Paul Chapman, 26-Oct-2012) (Proof shortened by Mario Carneiro, 13-Feb-2013)

	Ref	Expression
Assertion	hashsng	$$⊢A\in V\to \left|\left\{A\right\}\right|=1$$

Proof

Step	Hyp	Ref	Expression
1		1z	$$⊢1\in \mathbb{Z}$$
2		en2sn	$$⊢\left(A\in V\wedge 1\in \mathbb{Z}\right)\to \left\{A\right\}\approx \left\{1\right\}$$
3	1 2	mpan2	$$⊢A\in V\to \left\{A\right\}\approx \left\{1\right\}$$
4		snfi	$$⊢\left\{A\right\}\in \mathrm{Fin}$$
5		snfi	$$⊢\left\{1\right\}\in \mathrm{Fin}$$
6		hashen	$$⊢\left(\left\{A\right\}\in \mathrm{Fin}\wedge \left\{1\right\}\in \mathrm{Fin}\right)\to \left(\left|\left\{A\right\}\right|=\left|\left\{1\right\}\right|\leftrightarrow \left\{A\right\}\approx \left\{1\right\}\right)$$
7	4 5 6	mp2an	$$⊢\left|\left\{A\right\}\right|=\left|\left\{1\right\}\right|\leftrightarrow \left\{A\right\}\approx \left\{1\right\}$$
8	3 7	sylibr	$$⊢A\in V\to \left|\left\{A\right\}\right|=\left|\left\{1\right\}\right|$$
9		1nn0	$$⊢1\in {\mathbb{N}}_0$$
10		hashfz1	$$⊢1\in {\mathbb{N}}_0\to \left|\left(1\dots 1\right)\right|=1$$
11	9 10	ax-mp	$$⊢\left|\left(1\dots 1\right)\right|=1$$
12		fzsn	$$⊢1\in \mathbb{Z}\to \left(1\dots 1\right)=\left\{1\right\}$$
13	12	fveq2d	$$⊢1\in \mathbb{Z}\to \left|\left(1\dots 1\right)\right|=\left|\left\{1\right\}\right|$$
14	11 13	syl5reqr	$$⊢1\in \mathbb{Z}\to \left|\left\{1\right\}\right|=1$$
15	1 14	ax-mp	$$⊢\left|\left\{1\right\}\right|=1$$
16	8 15	syl6eq	$$⊢A\in V\to \left|\left\{A\right\}\right|=1$$