This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 < ( ♯ ‘ 𝐴 ) )