This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑥 𝑥 ∈ 𝑉 )