# Metamath Proof Explorer

## Theorem hashgt0elex

Description: If the size of a set is greater than zero, then the set must contain at least one element. (Contributed by Alexander van der Vekens, 6-Jan-2018)

Ref Expression
Assertion hashgt0elex ( ( 𝑉𝑊 ∧ 0 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑥 𝑥𝑉 )

### Proof

Step Hyp Ref Expression
1 alnex ( ∀ 𝑥 ¬ 𝑥𝑉 ↔ ¬ ∃ 𝑥 𝑥𝑉 )
2 eq0 ( 𝑉 = ∅ ↔ ∀ 𝑥 ¬ 𝑥𝑉 )
3 2 biimpri ( ∀ 𝑥 ¬ 𝑥𝑉𝑉 = ∅ )
4 3 a1d ( ∀ 𝑥 ¬ 𝑥𝑉 → ( 𝑉𝑊𝑉 = ∅ ) )
5 1 4 sylbir ( ¬ ∃ 𝑥 𝑥𝑉 → ( 𝑉𝑊𝑉 = ∅ ) )
6 5 impcom ( ( 𝑉𝑊 ∧ ¬ ∃ 𝑥 𝑥𝑉 ) → 𝑉 = ∅ )
7 hashle00 ( 𝑉𝑊 → ( ( ♯ ‘ 𝑉 ) ≤ 0 ↔ 𝑉 = ∅ ) )
8 7 adantr ( ( 𝑉𝑊 ∧ ¬ ∃ 𝑥 𝑥𝑉 ) → ( ( ♯ ‘ 𝑉 ) ≤ 0 ↔ 𝑉 = ∅ ) )
9 6 8 mpbird ( ( 𝑉𝑊 ∧ ¬ ∃ 𝑥 𝑥𝑉 ) → ( ♯ ‘ 𝑉 ) ≤ 0 )
10 hashxrcl ( 𝑉𝑊 → ( ♯ ‘ 𝑉 ) ∈ ℝ* )
11 0xr 0 ∈ ℝ*
12 xrlenlt ( ( ( ♯ ‘ 𝑉 ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( ♯ ‘ 𝑉 ) ≤ 0 ↔ ¬ 0 < ( ♯ ‘ 𝑉 ) ) )
13 10 11 12 sylancl ( 𝑉𝑊 → ( ( ♯ ‘ 𝑉 ) ≤ 0 ↔ ¬ 0 < ( ♯ ‘ 𝑉 ) ) )
14 13 bicomd ( 𝑉𝑊 → ( ¬ 0 < ( ♯ ‘ 𝑉 ) ↔ ( ♯ ‘ 𝑉 ) ≤ 0 ) )
15 14 adantr ( ( 𝑉𝑊 ∧ ¬ ∃ 𝑥 𝑥𝑉 ) → ( ¬ 0 < ( ♯ ‘ 𝑉 ) ↔ ( ♯ ‘ 𝑉 ) ≤ 0 ) )
16 9 15 mpbird ( ( 𝑉𝑊 ∧ ¬ ∃ 𝑥 𝑥𝑉 ) → ¬ 0 < ( ♯ ‘ 𝑉 ) )
17 16 ex ( 𝑉𝑊 → ( ¬ ∃ 𝑥 𝑥𝑉 → ¬ 0 < ( ♯ ‘ 𝑉 ) ) )
18 17 con4d ( 𝑉𝑊 → ( 0 < ( ♯ ‘ 𝑉 ) → ∃ 𝑥 𝑥𝑉 ) )
19 18 imp ( ( 𝑉𝑊 ∧ 0 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑥 𝑥𝑉 )