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 e. _V
Assertion	numth	|- E. x e. On E. f f : x -1-1-onto-> A

Proof

Step	Hyp	Ref	Expression
1		numth.1	|- A e. _V
2	1	numth2	|- E. x e. On x ~~ A
3		bren	|- ( x ~~ A <-> E. f f : x -1-1-onto-> A )
4	3	rexbii	|- ( E. x e. On x ~~ A <-> E. x e. On E. f f : x -1-1-onto-> A )
5	2 4	mpbi	|- E. x e. On E. f f : x -1-1-onto-> A