Metamath Proof Explorer

Theorem hashle00

Description: If the size of a set is less than or equal to zero, the set must be empty. (Contributed by Alexander van der Vekens, 6-Jan-2018) (Proof shortened by AV, 24-Oct-2021)

Ref Expression
Assertion hashle00 ⊢ V ∈ W → V ≤ 0 ↔ V = ∅

Proof

Step Hyp Ref Expression
1 hashge0 ⊢ V ∈ W → 0 ≤ V
2 1 biantrud ⊢ V ∈ W → V ≤ 0 ↔ V ≤ 0 ∧ 0 ≤ V
3 hashxrcl ⊢ V ∈ W → V ∈ ℝ *
4 0xr ⊢ 0 ∈ ℝ *
5 xrletri3 ⊢ V ∈ ℝ * ∧ 0 ∈ ℝ * → V = 0 ↔ V ≤ 0 ∧ 0 ≤ V
6 3 4 5 sylancl ⊢ V ∈ W → V = 0 ↔ V ≤ 0 ∧ 0 ≤ V
7 hasheq0 ⊢ V ∈ W → V = 0 ↔ V = ∅
8 2 6 7 3bitr2d ⊢ V ∈ W → V ≤ 0 ↔ V = ∅