# 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 ${⊢}{A}\in {V}\to \left|{A}\right|\ne \mathrm{-\infty }$

### Proof

Step Hyp Ref Expression
1 hashnn0pnf ${⊢}{A}\in {V}\to \left(\left|{A}\right|\in {ℕ}_{0}\vee \left|{A}\right|=\mathrm{+\infty }\right)$
2 mnfnre ${⊢}\mathrm{-\infty }\notin ℝ$
3 df-nel ${⊢}\mathrm{-\infty }\notin ℝ↔¬\mathrm{-\infty }\in ℝ$
4 nn0re ${⊢}\mathrm{-\infty }\in {ℕ}_{0}\to \mathrm{-\infty }\in ℝ$
5 4 con3i ${⊢}¬\mathrm{-\infty }\in ℝ\to ¬\mathrm{-\infty }\in {ℕ}_{0}$
6 3 5 sylbi ${⊢}\mathrm{-\infty }\notin ℝ\to ¬\mathrm{-\infty }\in {ℕ}_{0}$
7 2 6 ax-mp ${⊢}¬\mathrm{-\infty }\in {ℕ}_{0}$
8 eleq1 ${⊢}\left|{A}\right|=\mathrm{-\infty }\to \left(\left|{A}\right|\in {ℕ}_{0}↔\mathrm{-\infty }\in {ℕ}_{0}\right)$
9 7 8 mtbiri ${⊢}\left|{A}\right|=\mathrm{-\infty }\to ¬\left|{A}\right|\in {ℕ}_{0}$
10 9 necon2ai ${⊢}\left|{A}\right|\in {ℕ}_{0}\to \left|{A}\right|\ne \mathrm{-\infty }$
11 pnfnemnf ${⊢}\mathrm{+\infty }\ne \mathrm{-\infty }$
12 neeq1 ${⊢}\left|{A}\right|=\mathrm{+\infty }\to \left(\left|{A}\right|\ne \mathrm{-\infty }↔\mathrm{+\infty }\ne \mathrm{-\infty }\right)$
13 11 12 mpbiri ${⊢}\left|{A}\right|=\mathrm{+\infty }\to \left|{A}\right|\ne \mathrm{-\infty }$
14 10 13 jaoi ${⊢}\left(\left|{A}\right|\in {ℕ}_{0}\vee \left|{A}\right|=\mathrm{+\infty }\right)\to \left|{A}\right|\ne \mathrm{-\infty }$
15 1 14 syl ${⊢}{A}\in {V}\to \left|{A}\right|\ne \mathrm{-\infty }$