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 ⊢ A ∈ V ∧ A ≠ ∅ → 1 ≤ A

Proof

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