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	⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) ≠ -∞ )

Proof

Step	Hyp	Ref	Expression
1		hashnn0pnf	⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝐴 ) = +∞ ) )
2		mnfnre	⊢ -∞ ∉ ℝ
3		df-nel	⊢ ( -∞ ∉ ℝ ↔ ¬ -∞ ∈ ℝ )
4		nn0re	⊢ ( -∞ ∈ ℕ0 → -∞ ∈ ℝ )
5	4	con3i	⊢ ( ¬ -∞ ∈ ℝ → ¬ -∞ ∈ ℕ0 )
6	3 5	sylbi	⊢ ( -∞ ∉ ℝ → ¬ -∞ ∈ ℕ0 )
7	2 6	ax-mp	⊢ ¬ -∞ ∈ ℕ0
8		eleq1	⊢ ( ( ♯ ‘ 𝐴 ) = -∞ → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ↔ -∞ ∈ ℕ0 ) )
9	7 8	mtbiri	⊢ ( ( ♯ ‘ 𝐴 ) = -∞ → ¬ ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
10	9	necon2ai	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ♯ ‘ 𝐴 ) ≠ -∞ )
11		pnfnemnf	⊢ +∞ ≠ -∞
12		neeq1	⊢ ( ( ♯ ‘ 𝐴 ) = +∞ → ( ( ♯ ‘ 𝐴 ) ≠ -∞ ↔ +∞ ≠ -∞ ) )
13	11 12	mpbiri	⊢ ( ( ♯ ‘ 𝐴 ) = +∞ → ( ♯ ‘ 𝐴 ) ≠ -∞ )
14	10 13	jaoi	⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝐴 ) = +∞ ) → ( ♯ ‘ 𝐴 ) ≠ -∞ )
15	1 14	syl	⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) ≠ -∞ )