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	⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = 0 ↔ 𝐴 = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		pnfnre	⊢ +∞ ∉ ℝ
2	1	neli	⊢ ¬ +∞ ∈ ℝ
3		hashinf	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = +∞ )
4	3	eleq1d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) ∈ ℝ ↔ +∞ ∈ ℝ ) )
5	2 4	mtbiri	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ¬ ( ♯ ‘ 𝐴 ) ∈ ℝ )
6		id	⊢ ( ( ♯ ‘ 𝐴 ) = 0 → ( ♯ ‘ 𝐴 ) = 0 )
7		0re	⊢ 0 ∈ ℝ
8	6 7	eqeltrdi	⊢ ( ( ♯ ‘ 𝐴 ) = 0 → ( ♯ ‘ 𝐴 ) ∈ ℝ )
9	5 8	nsyl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ¬ ( ♯ ‘ 𝐴 ) = 0 )
10		id	⊢ ( 𝐴 = ∅ → 𝐴 = ∅ )
11		0fin	⊢ ∅ ∈ Fin
12	10 11	eqeltrdi	⊢ ( 𝐴 = ∅ → 𝐴 ∈ Fin )
13	12	con3i	⊢ ( ¬ 𝐴 ∈ Fin → ¬ 𝐴 = ∅ )
14	13	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ¬ 𝐴 = ∅ )
15	9 14	2falsed	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) = 0 ↔ 𝐴 = ∅ ) )
16	15	ex	⊢ ( 𝐴 ∈ 𝑉 → ( ¬ 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) = 0 ↔ 𝐴 = ∅ ) ) )
17		hashen	⊢ ( ( 𝐴 ∈ Fin ∧ ∅ ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ∅ ) ↔ 𝐴 ≈ ∅ ) )
18	11 17	mpan2	⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ∅ ) ↔ 𝐴 ≈ ∅ ) )
19		fz10	⊢ ( 1 ... 0 ) = ∅
20	19	fveq2i	⊢ ( ♯ ‘ ( 1 ... 0 ) ) = ( ♯ ‘ ∅ )
21		0nn0	⊢ 0 ∈ ℕ0
22		hashfz1	⊢ ( 0 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 0 ) ) = 0 )
23	21 22	ax-mp	⊢ ( ♯ ‘ ( 1 ... 0 ) ) = 0
24	20 23	eqtr3i	⊢ ( ♯ ‘ ∅ ) = 0
25	24	eqeq2i	⊢ ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ∅ ) ↔ ( ♯ ‘ 𝐴 ) = 0 )
26		en0	⊢ ( 𝐴 ≈ ∅ ↔ 𝐴 = ∅ )
27	18 25 26	3bitr3g	⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) = 0 ↔ 𝐴 = ∅ ) )
28	16 27	pm2.61d2	⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = 0 ↔ 𝐴 = ∅ ) )