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