Theorem numth2

Description: Numeration theorem: any set is equinumerous to some ordinal (using AC). Theorem 10.3 of TakeutiZaring p. 84. (Contributed by NM, 20-Oct-2003)

	Ref	Expression
Hypothesis	numth.1	$$⊢A\in \mathrm{V}$$
Assertion	numth2	$$⊢\exists x\in \mathrm{On}x\approx A$$

Proof

Step	Hyp	Ref	Expression
1		numth.1	$$⊢A\in \mathrm{V}$$
2		numth3	$$⊢A\in \mathrm{V}\to A\in \mathrm{dom}\mathrm{card}$$
3	1 2	ax-mp	$$⊢A\in \mathrm{dom}\mathrm{card}$$
4		isnum2	$$⊢A\in \mathrm{dom}\mathrm{card}\leftrightarrow \exists x\in \mathrm{On}x\approx A$$
5	3 4	mpbi	$$⊢\exists x\in \mathrm{On}x\approx A$$