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