hasheq0

Description: Two ways of saying a 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 (\|A\| = 0 \leftrightarrow A = \emptyset)$

Proof

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

Metamath Proof Explorer

Theorem hasheq0

Proof