# 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 ${⊢}\left({V}\in {W}\wedge 0<\left|{V}\right|\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {V}$

### Proof

Step Hyp Ref Expression
1 alnex ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}\in {V}↔¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {V}$
2 eq0 ${⊢}{V}=\varnothing ↔\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}\in {V}$
3 2 biimpri ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}\in {V}\to {V}=\varnothing$
4 3 a1d ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}\in {V}\to \left({V}\in {W}\to {V}=\varnothing \right)$
5 1 4 sylbir ${⊢}¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {V}\to \left({V}\in {W}\to {V}=\varnothing \right)$
6 5 impcom ${⊢}\left({V}\in {W}\wedge ¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {V}\right)\to {V}=\varnothing$
7 hashle00 ${⊢}{V}\in {W}\to \left(\left|{V}\right|\le 0↔{V}=\varnothing \right)$
8 7 adantr ${⊢}\left({V}\in {W}\wedge ¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {V}\right)\to \left(\left|{V}\right|\le 0↔{V}=\varnothing \right)$
9 6 8 mpbird ${⊢}\left({V}\in {W}\wedge ¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {V}\right)\to \left|{V}\right|\le 0$
10 hashxrcl ${⊢}{V}\in {W}\to \left|{V}\right|\in {ℝ}^{*}$
11 0xr ${⊢}0\in {ℝ}^{*}$
12 xrlenlt ${⊢}\left(\left|{V}\right|\in {ℝ}^{*}\wedge 0\in {ℝ}^{*}\right)\to \left(\left|{V}\right|\le 0↔¬0<\left|{V}\right|\right)$
13 10 11 12 sylancl ${⊢}{V}\in {W}\to \left(\left|{V}\right|\le 0↔¬0<\left|{V}\right|\right)$
14 13 bicomd ${⊢}{V}\in {W}\to \left(¬0<\left|{V}\right|↔\left|{V}\right|\le 0\right)$
15 14 adantr ${⊢}\left({V}\in {W}\wedge ¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {V}\right)\to \left(¬0<\left|{V}\right|↔\left|{V}\right|\le 0\right)$
16 9 15 mpbird ${⊢}\left({V}\in {W}\wedge ¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {V}\right)\to ¬0<\left|{V}\right|$
17 16 ex ${⊢}{V}\in {W}\to \left(¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {V}\to ¬0<\left|{V}\right|\right)$
18 17 con4d ${⊢}{V}\in {W}\to \left(0<\left|{V}\right|\to \exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {V}\right)$
19 18 imp ${⊢}\left({V}\in {W}\wedge 0<\left|{V}\right|\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}{x}\in {V}$