# Metamath Proof Explorer

## Theorem hashnnn0genn0

Description: If the size of a set is not a nonnegative integer, it is greater than or equal to any nonnegative integer. (Contributed by Alexander van der Vekens, 6-Dec-2017)

Ref Expression
Assertion hashnnn0genn0 ${⊢}\left({M}\in {V}\wedge \left|{M}\right|\notin {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {N}\le \left|{M}\right|$

### Proof

Step Hyp Ref Expression
1 df-nel ${⊢}\left|{M}\right|\notin {ℕ}_{0}↔¬\left|{M}\right|\in {ℕ}_{0}$
2 pm2.21 ${⊢}¬\left|{M}\right|\in {ℕ}_{0}\to \left(\left|{M}\right|\in {ℕ}_{0}\to {N}\le \left|{M}\right|\right)$
3 1 2 sylbi ${⊢}\left|{M}\right|\notin {ℕ}_{0}\to \left(\left|{M}\right|\in {ℕ}_{0}\to {N}\le \left|{M}\right|\right)$
4 3 3ad2ant2 ${⊢}\left({M}\in {V}\wedge \left|{M}\right|\notin {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left(\left|{M}\right|\in {ℕ}_{0}\to {N}\le \left|{M}\right|\right)$
5 nn0re ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℝ$
6 5 ltpnfd ${⊢}{N}\in {ℕ}_{0}\to {N}<\mathrm{+\infty }$
7 5 rexrd ${⊢}{N}\in {ℕ}_{0}\to {N}\in {ℝ}^{*}$
8 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
9 xrltle ${⊢}\left({N}\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left({N}<\mathrm{+\infty }\to {N}\le \mathrm{+\infty }\right)$
10 7 8 9 sylancl ${⊢}{N}\in {ℕ}_{0}\to \left({N}<\mathrm{+\infty }\to {N}\le \mathrm{+\infty }\right)$
11 6 10 mpd ${⊢}{N}\in {ℕ}_{0}\to {N}\le \mathrm{+\infty }$
12 breq2 ${⊢}\left|{M}\right|=\mathrm{+\infty }\to \left({N}\le \left|{M}\right|↔{N}\le \mathrm{+\infty }\right)$
13 11 12 syl5ibrcom ${⊢}{N}\in {ℕ}_{0}\to \left(\left|{M}\right|=\mathrm{+\infty }\to {N}\le \left|{M}\right|\right)$
14 13 3ad2ant3 ${⊢}\left({M}\in {V}\wedge \left|{M}\right|\notin {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left(\left|{M}\right|=\mathrm{+\infty }\to {N}\le \left|{M}\right|\right)$
15 hashnn0pnf ${⊢}{M}\in {V}\to \left(\left|{M}\right|\in {ℕ}_{0}\vee \left|{M}\right|=\mathrm{+\infty }\right)$
16 15 3ad2ant1 ${⊢}\left({M}\in {V}\wedge \left|{M}\right|\notin {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to \left(\left|{M}\right|\in {ℕ}_{0}\vee \left|{M}\right|=\mathrm{+\infty }\right)$
17 4 14 16 mpjaod ${⊢}\left({M}\in {V}\wedge \left|{M}\right|\notin {ℕ}_{0}\wedge {N}\in {ℕ}_{0}\right)\to {N}\le \left|{M}\right|$