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

Metamath Proof Explorer

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 ⊢ A ∈ V → 0 ≤ A

Proof

Step Hyp Ref Expression
1 0domg ⊢ A ∈ V → ∅ ≼ A
2 hashdomi ⊢ ∅ ≼ A → ∅ ≤ A
3 hash0 ⊢ ∅ = 0
4 3 breq1i ⊢ ∅ ≤ A ↔ 0 ≤ A
5 4 biimpi ⊢ ∅ ≤ A → 0 ≤ A
6 1 2 5 3syl ⊢ A ∈ V → 0 ≤ A