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