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

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 ⊢ M ∈ V ∧ M ∉ ℕ 0 ∧ N ∈ ℕ 0 → N ≤ M

Proof

Step Hyp Ref Expression
1 df-nel ⊢ M ∉ ℕ 0 ↔ ¬ M ∈ ℕ 0
2 pm2.21 ⊢ ¬ M ∈ ℕ 0 → M ∈ ℕ 0 → N ≤ M
3 1 2 sylbi ⊢ M ∉ ℕ 0 → M ∈ ℕ 0 → N ≤ M
4 3 3ad2ant2 ⊢ M ∈ V ∧ M ∉ ℕ 0 ∧ N ∈ ℕ 0 → M ∈ ℕ 0 → N ≤ M
5 nn0re ⊢ N ∈ ℕ 0 → N ∈ ℝ
6 5 ltpnfd ⊢ N ∈ ℕ 0 → N < +∞
7 5 rexrd ⊢ N ∈ ℕ 0 → N ∈ ℝ *
8 pnfxr ⊢ +∞ ∈ ℝ *
9 xrltle ⊢ N ∈ ℝ * ∧ +∞ ∈ ℝ * → N < +∞ → N ≤ +∞
10 7 8 9 sylancl ⊢ N ∈ ℕ 0 → N < +∞ → N ≤ +∞
11 6 10 mpd ⊢ N ∈ ℕ 0 → N ≤ +∞
12 breq2 ⊢ M = +∞ → N ≤ M ↔ N ≤ +∞
13 11 12 syl5ibrcom ⊢ N ∈ ℕ 0 → M = +∞ → N ≤ M
14 13 3ad2ant3 ⊢ M ∈ V ∧ M ∉ ℕ 0 ∧ N ∈ ℕ 0 → M = +∞ → N ≤ M
15 hashnn0pnf ⊢ M ∈ V → M ∈ ℕ 0 ∨ M = +∞
16 15 3ad2ant1 ⊢ M ∈ V ∧ M ∉ ℕ 0 ∧ N ∈ ℕ 0 → M ∈ ℕ 0 ∨ M = +∞
17 4 14 16 mpjaod ⊢ M ∈ V ∧ M ∉ ℕ 0 ∧ N ∈ ℕ 0 → N ≤ M