omiscard

		Ref	Expression
	Assertion	omiscard	$⊢ ω \in ran card$

Step	Hyp	Ref	Expression
1		omelon	$⊢ ω \in On$
2		nnsdom	$⊢ x \in ω \to x ≺ ω$
3		sdomnen	$⊢ x ≺ ω \to \neg x \approx ω$
4	2 3	syl	$⊢ x \in ω \to \neg x \approx ω$
5	4	rgen	$⊢ \forall x \in ω \neg x \approx ω$
6		elrncard	$⊢ ω \in ran card \leftrightarrow (ω \in On \land \forall x \in ω \neg x \approx ω)$
7	1 5 6	mpbir2an	$⊢ ω \in ran card$

Metamath Proof Explorer