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 ( ( 𝑀 ∈ 𝑉 ∧ ( ♯ ‘ 𝑀 ) ∉ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ≤ ( ♯ ‘ 𝑀 ) )

Proof

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