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

Metamath Proof Explorer

Theorem hashnemnf

Description: The size of a set is never minus infinity. (Contributed by Alexander van der Vekens, 21-Dec-2017)

Ref Expression
Assertion hashnemnf ( 𝐴 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) ≠ -∞ )

Proof

Step Hyp Ref Expression
1 hashnn0pnf ⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝐴 ) = +∞ ) )
2 mnfnre ⊢ -∞ ∉ ℝ
3 df-nel ⊢ ( -∞ ∉ ℝ ↔ ¬ -∞ ∈ ℝ )
4 nn0re ⊢ ( -∞ ∈ ℕ0 → -∞ ∈ ℝ )
5 4 con3i ⊢ ( ¬ -∞ ∈ ℝ → ¬ -∞ ∈ ℕ0 )
6 3 5 sylbi ⊢ ( -∞ ∉ ℝ → ¬ -∞ ∈ ℕ0 )
7 2 6 ax-mp ⊢ ¬ -∞ ∈ ℕ0
8 eleq1 ⊢ ( ( ♯ ‘ 𝐴 ) = -∞ → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ↔ -∞ ∈ ℕ0 ) )
9 7 8 mtbiri ⊢ ( ( ♯ ‘ 𝐴 ) = -∞ → ¬ ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
10 9 necon2ai ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ♯ ‘ 𝐴 ) ≠ -∞ )
11 pnfnemnf ⊢ +∞ ≠ -∞
12 neeq1 ⊢ ( ( ♯ ‘ 𝐴 ) = +∞ → ( ( ♯ ‘ 𝐴 ) ≠ -∞ ↔ +∞ ≠ -∞ ) )
13 11 12 mpbiri ⊢ ( ( ♯ ‘ 𝐴 ) = +∞ → ( ♯ ‘ 𝐴 ) ≠ -∞ )
14 10 13 jaoi ⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝐴 ) = +∞ ) → ( ♯ ‘ 𝐴 ) ≠ -∞ )
15 1 14 syl ⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) ≠ -∞ )