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 | ⊢ ( 𝑉 ∈ 𝑊 → ( ( ♯ ‘ 𝑉 ) ≤ 0 ↔ 𝑉 = ∅ ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hashge0 | ⊢ ( 𝑉 ∈ 𝑊 → 0 ≤ ( ♯ ‘ 𝑉 ) ) | |
| 2 | 1 | biantrud | ⊢ ( 𝑉 ∈ 𝑊 → ( ( ♯ ‘ 𝑉 ) ≤ 0 ↔ ( ( ♯ ‘ 𝑉 ) ≤ 0 ∧ 0 ≤ ( ♯ ‘ 𝑉 ) ) ) ) |
| 3 | hashxrcl | ⊢ ( 𝑉 ∈ 𝑊 → ( ♯ ‘ 𝑉 ) ∈ ℝ* ) | |
| 4 | 0xr | ⊢ 0 ∈ ℝ* | |
| 5 | xrletri3 | ⊢ ( ( ( ♯ ‘ 𝑉 ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( ♯ ‘ 𝑉 ) = 0 ↔ ( ( ♯ ‘ 𝑉 ) ≤ 0 ∧ 0 ≤ ( ♯ ‘ 𝑉 ) ) ) ) | |
| 6 | 3 4 5 | sylancl | ⊢ ( 𝑉 ∈ 𝑊 → ( ( ♯ ‘ 𝑉 ) = 0 ↔ ( ( ♯ ‘ 𝑉 ) ≤ 0 ∧ 0 ≤ ( ♯ ‘ 𝑉 ) ) ) ) |
| 7 | hasheq0 | ⊢ ( 𝑉 ∈ 𝑊 → ( ( ♯ ‘ 𝑉 ) = 0 ↔ 𝑉 = ∅ ) ) | |
| 8 | 2 6 7 | 3bitr2d | ⊢ ( 𝑉 ∈ 𝑊 → ( ( ♯ ‘ 𝑉 ) ≤ 0 ↔ 𝑉 = ∅ ) ) |