This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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