Theorem 1iscard

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

	Ref	Expression
Assertion	1iscard	$$⊢1_{𝑜}\in \mathrm{ran}\mathrm{card}$$

Proof

Step	Hyp	Ref	Expression
1		omssrncard	$$⊢\mathrm{\omega }\subseteq \mathrm{ran}\mathrm{card}$$
2		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
3	1 2	sselii	$$⊢1_{𝑜}\in \mathrm{ran}\mathrm{card}$$