Theorem hashneq0

Description: Two ways of saying a set is not empty. (Contributed by Alexander van der Vekens, 23-Sep-2018)

	Ref	Expression
Assertion	hashneq0	$$⊢A\in V\to \left(0<\left|A\right|\leftrightarrow A\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		hashnn0pnf	$$⊢A\in V\to \left(\left|A\right|\in {\mathbb{N}}_0\vee \left|A\right|=\mathrm{+\infty }\right)$$
2		nn0re	$$⊢\left|A\right|\in {\mathbb{N}}_0\to \left|A\right|\in ℝ$$
3		nn0ge0	$$⊢\left|A\right|\in {\mathbb{N}}_0\to 0\le \left|A\right|$$
4		ne0gt0	$$⊢\left(\left|A\right|\in ℝ\wedge 0\le \left|A\right|\right)\to \left(\left|A\right|\ne 0\leftrightarrow 0<\left|A\right|\right)$$
5	2 3 4	syl2anc	$$⊢\left|A\right|\in {\mathbb{N}}_0\to \left(\left|A\right|\ne 0\leftrightarrow 0<\left|A\right|\right)$$
6	5	bicomd	$$⊢\left|A\right|\in {\mathbb{N}}_0\to \left(0<\left|A\right|\leftrightarrow \left|A\right|\ne 0\right)$$
7		breq2	$$⊢\left|A\right|=\mathrm{+\infty }\to \left(0<\left|A\right|\leftrightarrow 0<\mathrm{+\infty }\right)$$
8		0ltpnf	$$⊢0<\mathrm{+\infty }$$
9		0re	$$⊢0\in ℝ$$
10		renepnf	$$⊢0\in ℝ\to 0\ne \mathrm{+\infty }$$
11	9 10	ax-mp	$$⊢0\ne \mathrm{+\infty }$$
12	11	necomi	$$⊢\mathrm{+\infty }\ne 0$$
13	8 12	2th	$$⊢0<\mathrm{+\infty }\leftrightarrow \mathrm{+\infty }\ne 0$$
14		neeq1	$$⊢\left|A\right|=\mathrm{+\infty }\to \left(\left|A\right|\ne 0\leftrightarrow \mathrm{+\infty }\ne 0\right)$$
15	13 14	bitr4id	$$⊢\left|A\right|=\mathrm{+\infty }\to \left(0<\mathrm{+\infty }\leftrightarrow \left|A\right|\ne 0\right)$$
16	7 15	bitrd	$$⊢\left|A\right|=\mathrm{+\infty }\to \left(0<\left|A\right|\leftrightarrow \left|A\right|\ne 0\right)$$
17	6 16	jaoi	$$⊢\left(\left|A\right|\in {\mathbb{N}}_0\vee \left|A\right|=\mathrm{+\infty }\right)\to \left(0<\left|A\right|\leftrightarrow \left|A\right|\ne 0\right)$$
18	1 17	syl	$$⊢A\in V\to \left(0<\left|A\right|\leftrightarrow \left|A\right|\ne 0\right)$$
19		hasheq0	$$⊢A\in V\to \left(\left|A\right|=0\leftrightarrow A=\varnothing \right)$$
20	19	necon3bid	$$⊢A\in V\to \left(\left|A\right|\ne 0\leftrightarrow A\ne \varnothing \right)$$
21	18 20	bitrd	$$⊢A\in V\to \left(0<\left|A\right|\leftrightarrow A\ne \varnothing \right)$$