Metamath Proof Explorer

Theorem bdayn0sf1o

Description: The birthday function restricted to the non-negative surreal integers is a bijection with the finite ordinals. (Contributed by Scott Fenton, 7-Nov-2025)

Ref Expression
Assertion bdayn0sf1o 
|- ( bday |` NN0_s ) : NN0_s -1-1-onto-> _om

Proof

Step Hyp Ref Expression
1 bdayfun 
 |-  Fun bday
2 funres 
 |-  ( Fun bday -> Fun ( bday |` NN0_s ) )
3 1 2 ax-mp 
 |-  Fun ( bday |` NN0_s )
4 dmres 
 |-  dom ( bday |` NN0_s ) = ( NN0_s i^i dom bday )
5 bdaydm 
 |-  dom bday = No
6 5 ineq2i 
 |-  ( NN0_s i^i dom bday ) = ( NN0_s i^i No )
7 n0ssno 
 |-  NN0_s C_ No
8 dfss2 
 |-  ( NN0_s C_ No <-> ( NN0_s i^i No ) = NN0_s )
9 7 8 mpbi 
 |-  ( NN0_s i^i No ) = NN0_s
10 4 6 9 3eqtri 
 |-  dom ( bday |` NN0_s ) = NN0_s
11 df-fn 
 |-  ( ( bday |` NN0_s ) Fn NN0_s <-> ( Fun ( bday |` NN0_s ) /\ dom ( bday |` NN0_s ) = NN0_s ) )
12 3 10 11 mpbir2an 
 |-  ( bday |` NN0_s ) Fn NN0_s
13 fvres 
 |-  ( x e. NN0_s -> ( ( bday |` NN0_s ) ` x ) = ( bday ` x ) )
14 n0sbday 
 |-  ( x e. NN0_s -> ( bday ` x ) e. _om )
15 13 14 eqeltrd 
 |-  ( x e. NN0_s -> ( ( bday |` NN0_s ) ` x ) e. _om )
16 15 rgen 
 |-  A. x e. NN0_s ( ( bday |` NN0_s ) ` x ) e. _om
17 fnfvrnss 
 |-  ( ( ( bday |` NN0_s ) Fn NN0_s /\ A. x e. NN0_s ( ( bday |` NN0_s ) ` x ) e. _om ) -> ran ( bday |` NN0_s ) C_ _om )
18 12 16 17 mp2an 
 |-  ran ( bday |` NN0_s ) C_ _om
19 eqeq2 
 |-  ( b = (/) -> ( ( bday ` y ) = b <-> ( bday ` y ) = (/) ) )
20 19 rexbidv 
 |-  ( b = (/) -> ( E. y e. NN0_s ( bday ` y ) = b <-> E. y e. NN0_s ( bday ` y ) = (/) ) )
21 eqeq2 
 |-  ( b = a -> ( ( bday ` y ) = b <-> ( bday ` y ) = a ) )
22 21 rexbidv 
 |-  ( b = a -> ( E. y e. NN0_s ( bday ` y ) = b <-> E. y e. NN0_s ( bday ` y ) = a ) )
23 eqeq2 
 |-  ( b = suc a -> ( ( bday ` y ) = b <-> ( bday ` y ) = suc a ) )
24 23 rexbidv 
 |-  ( b = suc a -> ( E. y e. NN0_s ( bday ` y ) = b <-> E. y e. NN0_s ( bday ` y ) = suc a ) )
25 fveqeq2 
 |-  ( y = z -> ( ( bday ` y ) = suc a <-> ( bday ` z ) = suc a ) )
26 25 cbvrexvw 
 |-  ( E. y e. NN0_s ( bday ` y ) = suc a <-> E. z e. NN0_s ( bday ` z ) = suc a )
27 24 26 bitrdi 
 |-  ( b = suc a -> ( E. y e. NN0_s ( bday ` y ) = b <-> E. z e. NN0_s ( bday ` z ) = suc a ) )
28 eqeq2 
 |-  ( b = x -> ( ( bday ` y ) = b <-> ( bday ` y ) = x ) )
29 28 rexbidv 
 |-  ( b = x -> ( E. y e. NN0_s ( bday ` y ) = b <-> E. y e. NN0_s ( bday ` y ) = x ) )
30 0n0s 
 |-  0s e. NN0_s
31 bday0s 
 |-  ( bday ` 0s ) = (/)
32 fveqeq2 
 |-  ( y = 0s -> ( ( bday ` y ) = (/) <-> ( bday ` 0s ) = (/) ) )
33 32 rspcev 
 |-  ( ( 0s e. NN0_s /\ ( bday ` 0s ) = (/) ) -> E. y e. NN0_s ( bday ` y ) = (/) )
34 30 31 33 mp2an 
 |-  E. y e. NN0_s ( bday ` y ) = (/)
35 fveqeq2 
 |-  ( z = ( y +s 1s ) -> ( ( bday ` z ) = suc ( bday ` y ) <-> ( bday ` ( y +s 1s ) ) = suc ( bday ` y ) ) )
36 peano2n0s 
 |-  ( y e. NN0_s -> ( y +s 1s ) e. NN0_s )
37 bdayn0p1 
 |-  ( y e. NN0_s -> ( bday ` ( y +s 1s ) ) = suc ( bday ` y ) )
38 35 36 37 rspcedvdw 
 |-  ( y e. NN0_s -> E. z e. NN0_s ( bday ` z ) = suc ( bday ` y ) )
39 38 adantl 
 |-  ( ( a e. _om /\ y e. NN0_s ) -> E. z e. NN0_s ( bday ` z ) = suc ( bday ` y ) )
40 suceq 
 |-  ( ( bday ` y ) = a -> suc ( bday ` y ) = suc a )
41 40 eqeq2d 
 |-  ( ( bday ` y ) = a -> ( ( bday ` z ) = suc ( bday ` y ) <-> ( bday ` z ) = suc a ) )
42 41 rexbidv 
 |-  ( ( bday ` y ) = a -> ( E. z e. NN0_s ( bday ` z ) = suc ( bday ` y ) <-> E. z e. NN0_s ( bday ` z ) = suc a ) )
43 39 42 syl5ibcom 
 |-  ( ( a e. _om /\ y e. NN0_s ) -> ( ( bday ` y ) = a -> E. z e. NN0_s ( bday ` z ) = suc a ) )
44 43 rexlimdva 
 |-  ( a e. _om -> ( E. y e. NN0_s ( bday ` y ) = a -> E. z e. NN0_s ( bday ` z ) = suc a ) )
45 20 22 27 29 34 44 finds 
 |-  ( x e. _om -> E. y e. NN0_s ( bday ` y ) = x )
46 fvelrnb 
 |-  ( ( bday |` NN0_s ) Fn NN0_s -> ( x e. ran ( bday |` NN0_s ) <-> E. y e. NN0_s ( ( bday |` NN0_s ) ` y ) = x ) )
47 12 46 ax-mp 
 |-  ( x e. ran ( bday |` NN0_s ) <-> E. y e. NN0_s ( ( bday |` NN0_s ) ` y ) = x )
48 fvres 
 |-  ( y e. NN0_s -> ( ( bday |` NN0_s ) ` y ) = ( bday ` y ) )
49 48 eqeq1d 
 |-  ( y e. NN0_s -> ( ( ( bday |` NN0_s ) ` y ) = x <-> ( bday ` y ) = x ) )
50 49 rexbiia 
 |-  ( E. y e. NN0_s ( ( bday |` NN0_s ) ` y ) = x <-> E. y e. NN0_s ( bday ` y ) = x )
51 47 50 bitri 
 |-  ( x e. ran ( bday |` NN0_s ) <-> E. y e. NN0_s ( bday ` y ) = x )
52 45 51 sylibr 
 |-  ( x e. _om -> x e. ran ( bday |` NN0_s ) )
53 52 ssriv 
 |-  _om C_ ran ( bday |` NN0_s )
54 18 53 eqssi 
 |-  ran ( bday |` NN0_s ) = _om
55 df-fo 
 |-  ( ( bday |` NN0_s ) : NN0_s -onto-> _om <-> ( ( bday |` NN0_s ) Fn NN0_s /\ ran ( bday |` NN0_s ) = _om ) )
56 12 54 55 mpbir2an 
 |-  ( bday |` NN0_s ) : NN0_s -onto-> _om
57 fof 
 |-  ( ( bday |` NN0_s ) : NN0_s -onto-> _om -> ( bday |` NN0_s ) : NN0_s --> _om )
58 56 57 ax-mp 
 |-  ( bday |` NN0_s ) : NN0_s --> _om
59 13 48 eqeqan12d 
 |-  ( ( x e. NN0_s /\ y e. NN0_s ) -> ( ( ( bday |` NN0_s ) ` x ) = ( ( bday |` NN0_s ) ` y ) <-> ( bday ` x ) = ( bday ` y ) ) )
60 n0ons 
 |-  ( x e. NN0_s -> x e. On_s )
61 n0ons 
 |-  ( y e. NN0_s -> y e. On_s )
62 bday11on 
 |-  ( ( x e. On_s /\ y e. On_s /\ ( bday ` x ) = ( bday ` y ) ) -> x = y )
63 62 3expia 
 |-  ( ( x e. On_s /\ y e. On_s ) -> ( ( bday ` x ) = ( bday ` y ) -> x = y ) )
64 60 61 63 syl2an 
 |-  ( ( x e. NN0_s /\ y e. NN0_s ) -> ( ( bday ` x ) = ( bday ` y ) -> x = y ) )
65 59 64 sylbid 
 |-  ( ( x e. NN0_s /\ y e. NN0_s ) -> ( ( ( bday |` NN0_s ) ` x ) = ( ( bday |` NN0_s ) ` y ) -> x = y ) )
66 65 rgen2 
 |-  A. x e. NN0_s A. y e. NN0_s ( ( ( bday |` NN0_s ) ` x ) = ( ( bday |` NN0_s ) ` y ) -> x = y )
67 dff13 
 |-  ( ( bday |` NN0_s ) : NN0_s -1-1-> _om <-> ( ( bday |` NN0_s ) : NN0_s --> _om /\ A. x e. NN0_s A. y e. NN0_s ( ( ( bday |` NN0_s ) ` x ) = ( ( bday |` NN0_s ) ` y ) -> x = y ) ) )
68 58 66 67 mpbir2an 
 |-  ( bday |` NN0_s ) : NN0_s -1-1-> _om
69 df-f1o 
 |-  ( ( bday |` NN0_s ) : NN0_s -1-1-onto-> _om <-> ( ( bday |` NN0_s ) : NN0_s -1-1-> _om /\ ( bday |` NN0_s ) : NN0_s -onto-> _om ) )
70 68 56 69 mpbir2an 
 |-  ( bday |` NN0_s ) : NN0_s -1-1-onto-> _om