Theorem bdayfo

Description: The birthday function maps the surreals onto the ordinals. Axiom B of Alling p. 184. (Proof shortened on 14-Apr-2012 by SF). (Contributed by Scott Fenton, 11-Jun-2011)

	Ref	Expression
Assertion	bdayfo	|- bday : No -onto-> On

Proof

Step	Hyp	Ref	Expression
1		dmexg	|- ( x e. No -> dom x e. _V )
2	1	rgen	|- A. x e. No dom x e. _V
3		df-bday	|- bday = ( x e. No |-> dom x )
4	3	mptfng	|- ( A. x e. No dom x e. _V <-> bday Fn No )
5	2 4	mpbi	|- bday Fn No
6	3	rnmpt	|- ran bday = { y | E. x e. No y = dom x }
7		noxp1o	|- ( y e. On -> ( y X. { 1o } ) e. No )
8		1oex	|- 1o e. _V
9	8	snnz	|- { 1o } =/= (/)
10		dmxp	|- ( { 1o } =/= (/) -> dom ( y X. { 1o } ) = y )
11	9 10	ax-mp	|- dom ( y X. { 1o } ) = y
12	11	eqcomi	|- y = dom ( y X. { 1o } )
13		dmeq	|- ( x = ( y X. { 1o } ) -> dom x = dom ( y X. { 1o } ) )
14	13	rspceeqv	|- ( ( ( y X. { 1o } ) e. No /\ y = dom ( y X. { 1o } ) ) -> E. x e. No y = dom x )
15	7 12 14	sylancl	|- ( y e. On -> E. x e. No y = dom x )
16		nodmon	|- ( x e. No -> dom x e. On )
17		eleq1a	|- ( dom x e. On -> ( y = dom x -> y e. On ) )
18	16 17	syl	|- ( x e. No -> ( y = dom x -> y e. On ) )
19	18	rexlimiv	|- ( E. x e. No y = dom x -> y e. On )
20	15 19	impbii	|- ( y e. On <-> E. x e. No y = dom x )
21	20	eqabi	|- On = { y | E. x e. No y = dom x }
22	6 21	eqtr4i	|- ran bday = On
23		df-fo	|- ( bday : No -onto-> On <-> ( bday Fn No /\ ran bday = On ) )
24	5 22 23	mpbir2an	|- bday : No -onto-> On