Theorem omiscard

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

	Ref	Expression
Assertion	omiscard	$$⊢\mathrm{\omega }\in \mathrm{ran}\mathrm{card}$$

Proof

Step	Hyp	Ref	Expression
1		omelon	$$⊢\mathrm{\omega }\in \mathrm{On}$$
2		nnsdom	$$⊢x\in \mathrm{\omega }\to x\prec \mathrm{\omega }$$
3		sdomnen	$$⊢x\prec \mathrm{\omega }\to \neg x\approx \mathrm{\omega }$$
4	2 3	syl	$$⊢x\in \mathrm{\omega }\to \neg x\approx \mathrm{\omega }$$
5	4	rgen	$$⊢\forall x\in \mathrm{\omega }\neg x\approx \mathrm{\omega }$$
6		elrncard	$$⊢\mathrm{\omega }\in \mathrm{ran}\mathrm{card}\leftrightarrow \left(\mathrm{\omega }\in \mathrm{On}\wedge \forall x\in \mathrm{\omega }\neg x\approx \mathrm{\omega }\right)$$
7	1 5 6	mpbir2an	$$⊢\mathrm{\omega }\in \mathrm{ran}\mathrm{card}$$