Theorem numth

Description: Numeration theorem: every set can be put into one-to-one correspondence with some ordinal (using AC). Theorem 10.3 of TakeutiZaring p. 84. (Contributed by NM, 10-Feb-1997) (Proof shortened by Mario Carneiro, 8-Jan-2015)

	Ref	Expression
Hypothesis	numth.1	$$⊢A\in \mathrm{V}$$
Assertion	numth	$$⊢\exists x\in \mathrm{On}\exists ff:x\underset{1-1\; onto}{⟶}A$$

Proof

Step	Hyp	Ref	Expression
1		numth.1	$$⊢A\in \mathrm{V}$$
2	1	numth2	$$⊢\exists x\in \mathrm{On}x\approx A$$
3		bren	$$⊢x\approx A\leftrightarrow \exists ff:x\underset{1-1\; onto}{⟶}A$$
4	3	rexbii	$$⊢\exists x\in \mathrm{On}x\approx A\leftrightarrow \exists x\in \mathrm{On}\exists ff:x\underset{1-1\; onto}{⟶}A$$
5	2 4	mpbi	$$⊢\exists x\in \mathrm{On}\exists ff:x\underset{1-1\; onto}{⟶}A$$