Theorem hasheq0

Description: Two ways of saying a finite set is empty. (Contributed by Paul Chapman, 26-Oct-2012) (Revised by Mario Carneiro, 27-Jul-2014)

	Ref	Expression
Assertion	hasheq0	$$⊢A\in V\to \left(\left|A\right|=0\leftrightarrow A=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		pnfnre	$$⊢\mathrm{+\infty }\notin ℝ$$
2	1	neli	$$⊢\neg \mathrm{+\infty }\in ℝ$$
3		hashinf	$$⊢\left(A\in V\wedge \neg A\in \mathrm{Fin}\right)\to \left|A\right|=\mathrm{+\infty }$$
4	3	eleq1d	$$⊢\left(A\in V\wedge \neg A\in \mathrm{Fin}\right)\to \left(\left|A\right|\in ℝ\leftrightarrow \mathrm{+\infty }\in ℝ\right)$$
5	2 4	mtbiri	$$⊢\left(A\in V\wedge \neg A\in \mathrm{Fin}\right)\to \neg \left|A\right|\in ℝ$$
6		id	$$⊢\left|A\right|=0\to \left|A\right|=0$$
7		0re	$$⊢0\in ℝ$$
8	6 7	eqeltrdi	$$⊢\left|A\right|=0\to \left|A\right|\in ℝ$$
9	5 8	nsyl	$$⊢\left(A\in V\wedge \neg A\in \mathrm{Fin}\right)\to \neg \left|A\right|=0$$
10		id	$$⊢A=\varnothing \to A=\varnothing$$
11		0fin	$$⊢\varnothing \in \mathrm{Fin}$$
12	10 11	eqeltrdi	$$⊢A=\varnothing \to A\in \mathrm{Fin}$$
13	12	con3i	$$⊢\neg A\in \mathrm{Fin}\to \neg A=\varnothing$$
14	13	adantl	$$⊢\left(A\in V\wedge \neg A\in \mathrm{Fin}\right)\to \neg A=\varnothing$$
15	9 14	2falsed	$$⊢\left(A\in V\wedge \neg A\in \mathrm{Fin}\right)\to \left(\left|A\right|=0\leftrightarrow A=\varnothing \right)$$
16	15	ex	$$⊢A\in V\to \left(\neg A\in \mathrm{Fin}\to \left(\left|A\right|=0\leftrightarrow A=\varnothing \right)\right)$$
17		hashen	$$⊢\left(A\in \mathrm{Fin}\wedge \varnothing \in \mathrm{Fin}\right)\to \left(\left|A\right|=\left|\varnothing \right|\leftrightarrow A\approx \varnothing \right)$$
18	11 17	mpan2	$$⊢A\in \mathrm{Fin}\to \left(\left|A\right|=\left|\varnothing \right|\leftrightarrow A\approx \varnothing \right)$$
19		fz10	$$⊢\left(1\dots 0\right)=\varnothing$$
20	19	fveq2i	$$⊢\left|\left(1\dots 0\right)\right|=\left|\varnothing \right|$$
21		0nn0	$$⊢0\in {\mathbb{N}}_0$$
22		hashfz1	$$⊢0\in {\mathbb{N}}_0\to \left|\left(1\dots 0\right)\right|=0$$
23	21 22	ax-mp	$$⊢\left|\left(1\dots 0\right)\right|=0$$
24	20 23	eqtr3i	$$⊢\left|\varnothing \right|=0$$
25	24	eqeq2i	$$⊢\left|A\right|=\left|\varnothing \right|\leftrightarrow \left|A\right|=0$$
26		en0	$$⊢A\approx \varnothing \leftrightarrow A=\varnothing$$
27	18 25 26	3bitr3g	$$⊢A\in \mathrm{Fin}\to \left(\left|A\right|=0\leftrightarrow A=\varnothing \right)$$
28	16 27	pm2.61d2	$$⊢A\in V\to \left(\left|A\right|=0\leftrightarrow A=\varnothing \right)$$