Theorem hashgt0

Description: The cardinality of a nonempty set is greater than zero. (Contributed by Thierry Arnoux, 2-Mar-2017)

	Ref	Expression
Assertion	hashgt0	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → 0 < ( ♯ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		hashge0	⊢ ( 𝐴 ∈ 𝑉 → 0 ≤ ( ♯ ‘ 𝐴 ) )
2	1	adantr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → 0 ≤ ( ♯ ‘ 𝐴 ) )
3		hasheq0	⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = 0 ↔ 𝐴 = ∅ ) )
4	3	necon3bid	⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ ∅ ) )
5	4	biimpar	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ( ♯ ‘ 𝐴 ) ≠ 0 )
6	2 5	jca	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ( 0 ≤ ( ♯ ‘ 𝐴 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) )
7		0xr	⊢ 0 ∈ ℝ*
8		hashxrcl	⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℝ* )
9		xrltlen	⊢ ( ( 0 ∈ ℝ* ∧ ( ♯ ‘ 𝐴 ) ∈ ℝ* ) → ( 0 < ( ♯ ‘ 𝐴 ) ↔ ( 0 ≤ ( ♯ ‘ 𝐴 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ) )
10	7 8 9	sylancr	⊢ ( 𝐴 ∈ 𝑉 → ( 0 < ( ♯ ‘ 𝐴 ) ↔ ( 0 ≤ ( ♯ ‘ 𝐴 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ) )
11	10	biimpar	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 0 ≤ ( ♯ ‘ 𝐴 ) ∧ ( ♯ ‘ 𝐴 ) ≠ 0 ) ) → 0 < ( ♯ ‘ 𝐴 ) )
12	6 11	syldan	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → 0 < ( ♯ ‘ 𝐴 ) )