Theorem onenon

Description: Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015)

	Ref	Expression
Assertion	onenon	$$⊢A\in \mathrm{On}\to A\in \mathrm{dom}\mathrm{card}$$

Proof

Step	Hyp	Ref	Expression
1		enrefg	$$⊢A\in \mathrm{On}\to A\approx A$$
2		isnumi	$$⊢\left(A\in \mathrm{On}\wedge A\approx A\right)\to A\in \mathrm{dom}\mathrm{card}$$
3	1 2	mpdan	$$⊢A\in \mathrm{On}\to A\in \mathrm{dom}\mathrm{card}$$