Theorem hashge0

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

	Ref	Expression
Assertion	hashge0	⊢ ( 𝐴 ∈ 𝑉 → 0 ≤ ( ♯ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		0domg	⊢ ( 𝐴 ∈ 𝑉 → ∅ ≼ 𝐴 )
2		hashdomi	⊢ ( ∅ ≼ 𝐴 → ( ♯ ‘ ∅ ) ≤ ( ♯ ‘ 𝐴 ) )
3		hash0	⊢ ( ♯ ‘ ∅ ) = 0
4	3	breq1i	⊢ ( ( ♯ ‘ ∅ ) ≤ ( ♯ ‘ 𝐴 ) ↔ 0 ≤ ( ♯ ‘ 𝐴 ) )
5	4	biimpi	⊢ ( ( ♯ ‘ ∅ ) ≤ ( ♯ ‘ 𝐴 ) → 0 ≤ ( ♯ ‘ 𝐴 ) )
6	1 2 5	3syl	⊢ ( 𝐴 ∈ 𝑉 → 0 ≤ ( ♯ ‘ 𝐴 ) )