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 ⊢ V ∈ W ∧ 0 < V → ∃ x x ∈ V

Proof

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