Metamath Proof Explorer


Theorem bdayfo

Description: The birthday function maps the surreals onto the ordinals. Axiom B of Alling p. 184. (Shortened proof on 2012-Apr-14, 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 abbi2i
 |-  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