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 xx\in V$$

Proof

Step	Hyp	Ref	Expression
1		alnex	$$⊢\forall x\neg x\in V\leftrightarrow \neg \exists xx\in V$$
2		eq0	$$⊢V=\varnothing \leftrightarrow \forall x\neg x\in V$$
3	2	biimpri	$$⊢\forall x\neg x\in V\to V=\varnothing$$
4	3	a1d	$$⊢\forall x\neg x\in V\to \left(V\in W\to V=\varnothing \right)$$
5	1 4	sylbir	$$⊢\neg \exists xx\in V\to \left(V\in W\to V=\varnothing \right)$$
6	5	impcom	$$⊢\left(V\in W\wedge \neg \exists xx\in V\right)\to V=\varnothing$$
7		hashle00	$$⊢V\in W\to \left(\left|V\right|\le 0\leftrightarrow V=\varnothing \right)$$
8	7	adantr	$$⊢\left(V\in W\wedge \neg \exists xx\in V\right)\to \left(\left|V\right|\le 0\leftrightarrow V=\varnothing \right)$$
9	6 8	mpbird	$$⊢\left(V\in W\wedge \neg \exists xx\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\leftrightarrow \neg 0<\left|V\right|\right)$$
13	10 11 12	sylancl	$$⊢V\in W\to \left(\left|V\right|\le 0\leftrightarrow \neg 0<\left|V\right|\right)$$
14	13	bicomd	$$⊢V\in W\to \left(\neg 0<\left|V\right|\leftrightarrow \left|V\right|\le 0\right)$$
15	14	adantr	$$⊢\left(V\in W\wedge \neg \exists xx\in V\right)\to \left(\neg 0<\left|V\right|\leftrightarrow \left|V\right|\le 0\right)$$
16	9 15	mpbird	$$⊢\left(V\in W\wedge \neg \exists xx\in V\right)\to \neg 0<\left|V\right|$$
17	16	ex	$$⊢V\in W\to \left(\neg \exists xx\in V\to \neg 0<\left|V\right|\right)$$
18	17	con4d	$$⊢V\in W\to \left(0<\left|V\right|\to \exists xx\in V\right)$$
19	18	imp	$$⊢\left(V\in W\wedge 0<\left|V\right|\right)\to \exists xx\in V$$