Metamath Proof Explorer


Theorem 0iscard

Description: 0 is a cardinal number. (Contributed by RP, 1-Oct-2023)

Ref Expression
Assertion 0iscard ⊢ ∅ ∈ ran ⁡ card

Proof

Step Hyp Ref Expression
1 omssrncard ⊢ ω ⊆ ran ⁡ card
2 peano1 ⊢ ∅ ∈ ω
3 1 2 sselii ⊢ ∅ ∈ ran ⁡ card