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

Metamath Proof Explorer

Theorem hashge1

Description: The cardinality of a nonempty set is greater than or equal to one. (Contributed by Thierry Arnoux, 20-Jun-2017)

Ref Expression
Assertion hashge1 ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → 1 ≤ ( ♯ ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) ∧ 𝐴 ∈ Fin ) → 𝐴 ∈ Fin )
2 simplr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) ∧ 𝐴 ∈ Fin ) → 𝐴 ≠ ∅ )
3 hashnncl ⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ 𝐴 ≠ ∅ ) )
4 3 biimpar ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
5 1 2 4 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) ∧ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
6 5 nnge1d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) ∧ 𝐴 ∈ Fin ) → 1 ≤ ( ♯ ‘ 𝐴 ) )
7 1xr ⊢ 1 ∈ ℝ*
8 pnfge ⊢ ( 1 ∈ ℝ* → 1 ≤ +∞ )
9 7 8 ax-mp ⊢ 1 ≤ +∞
10 hashinf ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = +∞ )
11 10 adantlr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = +∞ )
12 9 11 breqtrrid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) ∧ ¬ 𝐴 ∈ Fin ) → 1 ≤ ( ♯ ‘ 𝐴 ) )
13 6 12 pm2.61dan ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → 1 ≤ ( ♯ ‘ 𝐴 ) )