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 ) → 𝑁 ≤ ( ♯ ‘ 𝑀 ) )