Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 hashnn0pnf ⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝐴 ) = +∞ ) )
2 nn0re ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ♯ ‘ 𝐴 ) ∈ ℝ )
3 nn0ge0 ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → 0 ≤ ( ♯ ‘ 𝐴 ) )
4 ne0gt0 ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( ♯ ‘ 𝐴 ) ) → ( ( ♯ ‘ 𝐴 ) ≠ 0 ↔ 0 < ( ♯ ‘ 𝐴 ) ) )
5 2 3 4 syl2anc ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐴 ) ≠ 0 ↔ 0 < ( ♯ ‘ 𝐴 ) ) )
6 5 bicomd ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( 0 < ( ♯ ‘ 𝐴 ) ↔ ( ♯ ‘ 𝐴 ) ≠ 0 ) )
7 breq2 ⊢ ( ( ♯ ‘ 𝐴 ) = +∞ → ( 0 < ( ♯ ‘ 𝐴 ) ↔ 0 < +∞ ) )
8 0ltpnf ⊢ 0 < +∞
9 0re ⊢ 0 ∈ ℝ
10 renepnf ⊢ ( 0 ∈ ℝ → 0 ≠ +∞ )
11 9 10 ax-mp ⊢ 0 ≠ +∞
12 11 necomi ⊢ +∞ ≠ 0
13 8 12 2th ⊢ ( 0 < +∞ ↔ +∞ ≠ 0 )
14 neeq1 ⊢ ( ( ♯ ‘ 𝐴 ) = +∞ → ( ( ♯ ‘ 𝐴 ) ≠ 0 ↔ +∞ ≠ 0 ) )
15 13 14 bitr4id ⊢ ( ( ♯ ‘ 𝐴 ) = +∞ → ( 0 < +∞ ↔ ( ♯ ‘ 𝐴 ) ≠ 0 ) )
16 7 15 bitrd ⊢ ( ( ♯ ‘ 𝐴 ) = +∞ → ( 0 < ( ♯ ‘ 𝐴 ) ↔ ( ♯ ‘ 𝐴 ) ≠ 0 ) )
17 6 16 jaoi ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝐴 ) = +∞ ) → ( 0 < ( ♯ ‘ 𝐴 ) ↔ ( ♯ ‘ 𝐴 ) ≠ 0 ) )
18 1 17 syl ⊢ ( 𝐴 ∈ 𝑉 → ( 0 < ( ♯ ‘ 𝐴 ) ↔ ( ♯ ‘ 𝐴 ) ≠ 0 ) )
19 hasheq0 ⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = 0 ↔ 𝐴 = ∅ ) )
20 19 necon3bid ⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ ∅ ) )
21 18 20 bitrd ⊢ ( 𝐴 ∈ 𝑉 → ( 0 < ( ♯ ‘ 𝐴 ) ↔ 𝐴 ≠ ∅ ) )