Metamath Proof Explorer

Theorem onsiso

Description: The birthday function restricted to the surreal ordinals forms an order-preserving isomorphism with the regular ordinals. (Contributed by Scott Fenton, 8-Nov-2025)

Ref Expression
Assertion onsiso 
|- ( bday |` On_s ) Isom

Proof

Step Hyp Ref Expression
1 bdayfun 
 |-  Fun bday
2 funres 
 |-  ( Fun bday -> Fun ( bday |` On_s ) )
3 1 2 ax-mp 
 |-  Fun ( bday |` On_s )
4 dmres 
 |-  dom ( bday |` On_s ) = ( On_s i^i dom bday )
5 bdaydm 
 |-  dom bday = No
6 5 ineq2i 
 |-  ( On_s i^i dom bday ) = ( On_s i^i No )
7 onssno 
 |-  On_s C_ No
8 dfss2 
 |-  ( On_s C_ No <-> ( On_s i^i No ) = On_s )
9 7 8 mpbi 
 |-  ( On_s i^i No ) = On_s
10 4 6 9 3eqtri 
 |-  dom ( bday |` On_s ) = On_s
11 df-fn 
 |-  ( ( bday |` On_s ) Fn On_s <-> ( Fun ( bday |` On_s ) /\ dom ( bday |` On_s ) = On_s ) )
12 3 10 11 mpbir2an 
 |-  ( bday |` On_s ) Fn On_s
13 rnresss 
 |-  ran ( bday |` On_s ) C_ ran bday
14 bdayrn 
 |-  ran bday = On
15 13 14 sseqtri 
 |-  ran ( bday |` On_s ) C_ On
16 df-f 
 |-  ( ( bday |` On_s ) : On_s --> On <-> ( ( bday |` On_s ) Fn On_s /\ ran ( bday |` On_s ) C_ On ) )
17 12 15 16 mpbir2an 
 |-  ( bday |` On_s ) : On_s --> On
18 fvres 
 |-  ( x e. On_s -> ( ( bday |` On_s ) ` x ) = ( bday ` x ) )
19 fvres 
 |-  ( y e. On_s -> ( ( bday |` On_s ) ` y ) = ( bday ` y ) )
20 18 19 eqeqan12d 
 |-  ( ( x e. On_s /\ y e. On_s ) -> ( ( ( bday |` On_s ) ` x ) = ( ( bday |` On_s ) ` y ) <-> ( bday ` x ) = ( bday ` y ) ) )
21 bday11on 
 |-  ( ( x e. On_s /\ y e. On_s /\ ( bday ` x ) = ( bday ` y ) ) -> x = y )
22 21 3expia 
 |-  ( ( x e. On_s /\ y e. On_s ) -> ( ( bday ` x ) = ( bday ` y ) -> x = y ) )
23 20 22 sylbid 
 |-  ( ( x e. On_s /\ y e. On_s ) -> ( ( ( bday |` On_s ) ` x ) = ( ( bday |` On_s ) ` y ) -> x = y ) )
24 23 rgen2 
 |-  A. x e. On_s A. y e. On_s ( ( ( bday |` On_s ) ` x ) = ( ( bday |` On_s ) ` y ) -> x = y )
25 dff13 
 |-  ( ( bday |` On_s ) : On_s -1-1-> On <-> ( ( bday |` On_s ) : On_s --> On /\ A. x e. On_s A. y e. On_s ( ( ( bday |` On_s ) ` x ) = ( ( bday |` On_s ) ` y ) -> x = y ) ) )
26 17 24 25 mpbir2an 
 |-  ( bday |` On_s ) : On_s -1-1-> On
27 fveqeq2 
 |-  ( y = ( ( _Old ` x ) |s (/) ) -> ( ( ( bday |` On_s ) ` y ) = x <-> ( ( bday |` On_s ) ` ( ( _Old ` x ) |s (/) ) ) = x ) )
28 fvex 
 |-  ( _Old ` x ) e. _V
29 28 a1i 
 |-  ( x e. On -> ( _Old ` x ) e. _V )
30 oldssno 
 |-  ( _Old ` x ) C_ No
31 30 a1i 
 |-  ( x e. On -> ( _Old ` x ) C_ No )
32 eqidd 
 |-  ( x e. On -> ( ( _Old ` x ) |s (/) ) = ( ( _Old ` x ) |s (/) ) )
33 29 31 32 elons2d 
 |-  ( x e. On -> ( ( _Old ` x ) |s (/) ) e. On_s )
34 33 fvresd 
 |-  ( x e. On -> ( ( bday |` On_s ) ` ( ( _Old ` x ) |s (/) ) ) = ( bday ` ( ( _Old ` x ) |s (/) ) ) )
35 28 elpw 
 |-  ( ( _Old ` x ) e. ~P No <-> ( _Old ` x ) C_ No )
36 30 35 mpbir 
 |-  ( _Old ` x ) e. ~P No
37 nulssgt 
 |-  ( ( _Old ` x ) e. ~P No -> ( _Old ` x ) <
38 36 37 ax-mp 
 |-  ( _Old ` x ) <
39 id 
 |-  ( x e. On -> x e. On )
40 un0 
 |-  ( ( _Old ` x ) u. (/) ) = ( _Old ` x )
41 40 imaeq2i 
 |-  ( bday " ( ( _Old ` x ) u. (/) ) ) = ( bday " ( _Old ` x ) )
42 oldbdayim 
 |-  ( y e. ( _Old ` x ) -> ( bday ` y ) e. x )
43 42 rgen 
 |-  A. y e. ( _Old ` x ) ( bday ` y ) e. x
44 43 a1i 
 |-  ( x e. On -> A. y e. ( _Old ` x ) ( bday ` y ) e. x )
45 30 5 sseqtrri 
 |-  ( _Old ` x ) C_ dom bday
46 funimass4 
 |-  ( ( Fun bday /\ ( _Old ` x ) C_ dom bday ) -> ( ( bday " ( _Old ` x ) ) C_ x <-> A. y e. ( _Old ` x ) ( bday ` y ) e. x ) )
47 1 45 46 mp2an 
 |-  ( ( bday " ( _Old ` x ) ) C_ x <-> A. y e. ( _Old ` x ) ( bday ` y ) e. x )
48 44 47 sylibr 
 |-  ( x e. On -> ( bday " ( _Old ` x ) ) C_ x )
49 41 48 eqsstrid 
 |-  ( x e. On -> ( bday " ( ( _Old ` x ) u. (/) ) ) C_ x )
50 scutbdaybnd 
 |-  ( ( ( _Old ` x ) < ( bday ` ( ( _Old ` x ) |s (/) ) ) C_ x )
51 38 39 49 50 mp3an2i 
 |-  ( x e. On -> ( bday ` ( ( _Old ` x ) |s (/) ) ) C_ x )
52 ssltsep 
 |-  ( ( _Old ` x ) < A. y e. ( _Old ` x ) A. z e. { w } y
53 vex 
 |-  w e. _V
54 breq2 
 |-  ( z = w -> ( y  y
55 53 54 ralsn 
 |-  ( A. z e. { w } y  y
56 55 ralbii 
 |-  ( A. y e. ( _Old ` x ) A. z e. { w } y  A. y e. ( _Old ` x ) y
57 52 56 sylib 
 |-  ( ( _Old ` x ) < A. y e. ( _Old ` x ) y
58 sltirr 
 |-  ( w e. No -> -. w
59 58 3ad2ant2 
 |-  ( ( x e. On /\ w e. No /\ A. y e. ( _Old ` x ) y  -. w
60 oldbday 
 |-  ( ( x e. On /\ w e. No ) -> ( w e. ( _Old ` x ) <-> ( bday ` w ) e. x ) )
61 60 3adant3 
 |-  ( ( x e. On /\ w e. No /\ A. y e. ( _Old ` x ) y  ( w e. ( _Old ` x ) <-> ( bday ` w ) e. x ) )
62 breq1 
 |-  ( y = w -> ( y  w
63 62 rspccv 
 |-  ( A. y e. ( _Old ` x ) y  ( w e. ( _Old ` x ) -> w
64 63 3ad2ant3 
 |-  ( ( x e. On /\ w e. No /\ A. y e. ( _Old ` x ) y  ( w e. ( _Old ` x ) -> w
65 61 64 sylbird 
 |-  ( ( x e. On /\ w e. No /\ A. y e. ( _Old ` x ) y  ( ( bday ` w ) e. x -> w
66 59 65 mtod 
 |-  ( ( x e. On /\ w e. No /\ A. y e. ( _Old ` x ) y  -. ( bday ` w ) e. x )
67 simp1 
 |-  ( ( x e. On /\ w e. No /\ A. y e. ( _Old ` x ) y  x e. On )
68 bdayelon 
 |-  ( bday ` w ) e. On
69 ontri1 
 |-  ( ( x e. On /\ ( bday ` w ) e. On ) -> ( x C_ ( bday ` w ) <-> -. ( bday ` w ) e. x ) )
70 67 68 69 sylancl 
 |-  ( ( x e. On /\ w e. No /\ A. y e. ( _Old ` x ) y  ( x C_ ( bday ` w ) <-> -. ( bday ` w ) e. x ) )
71 66 70 mpbird 
 |-  ( ( x e. On /\ w e. No /\ A. y e. ( _Old ` x ) y  x C_ ( bday ` w ) )
72 71 3expia 
 |-  ( ( x e. On /\ w e. No ) -> ( A. y e. ( _Old ` x ) y  x C_ ( bday ` w ) ) )
73 57 72 syl5 
 |-  ( ( x e. On /\ w e. No ) -> ( ( _Old ` x ) < x C_ ( bday ` w ) ) )
74 73 adantrd 
 |-  ( ( x e. On /\ w e. No ) -> ( ( ( _Old ` x ) < x C_ ( bday ` w ) ) )
75 74 ralrimiva 
 |-  ( x e. On -> A. w e. No ( ( ( _Old ` x ) < x C_ ( bday ` w ) ) )
76 ssint 
 |-  ( x C_ |^| ( bday " { y e. No | ( ( _Old ` x ) < A. z e. ( bday " { y e. No | ( ( _Old ` x ) <
77 bdayfn 
 |-  bday Fn No
78 ssrab2 
 |-  { y e. No | ( ( _Old ` x ) <
79 sseq2 
 |-  ( z = ( bday ` w ) -> ( x C_ z <-> x C_ ( bday ` w ) ) )
80 79 ralima 
 |-  ( ( bday Fn No /\ { y e. No | ( ( _Old ` x ) < ( A. z e. ( bday " { y e. No | ( ( _Old ` x ) < A. w e. { y e. No | ( ( _Old ` x ) <
81 77 78 80 mp2an 
 |-  ( A. z e. ( bday " { y e. No | ( ( _Old ` x ) < A. w e. { y e. No | ( ( _Old ` x ) <
82 sneq 
 |-  ( y = w -> { y } = { w } )
83 82 breq2d 
 |-  ( y = w -> ( ( _Old ` x ) < ( _Old ` x ) <
84 82 breq1d 
 |-  ( y = w -> ( { y } < { w } <
85 83 84 anbi12d 
 |-  ( y = w -> ( ( ( _Old ` x ) < ( ( _Old ` x ) <
86 85 ralrab 
 |-  ( A. w e. { y e. No | ( ( _Old ` x ) < A. w e. No ( ( ( _Old ` x ) < x C_ ( bday ` w ) ) )
87 76 81 86 3bitri 
 |-  ( x C_ |^| ( bday " { y e. No | ( ( _Old ` x ) < A. w e. No ( ( ( _Old ` x ) < x C_ ( bday ` w ) ) )
88 75 87 sylibr 
 |-  ( x e. On -> x C_ |^| ( bday " { y e. No | ( ( _Old ` x ) <
89 scutbday 
 |-  ( ( _Old ` x ) < ( bday ` ( ( _Old ` x ) |s (/) ) ) = |^| ( bday " { y e. No | ( ( _Old ` x ) <
90 38 89 ax-mp 
 |-  ( bday ` ( ( _Old ` x ) |s (/) ) ) = |^| ( bday " { y e. No | ( ( _Old ` x ) <
91 88 90 sseqtrrdi 
 |-  ( x e. On -> x C_ ( bday ` ( ( _Old ` x ) |s (/) ) ) )
92 51 91 eqssd 
 |-  ( x e. On -> ( bday ` ( ( _Old ` x ) |s (/) ) ) = x )
93 34 92 eqtrd 
 |-  ( x e. On -> ( ( bday |` On_s ) ` ( ( _Old ` x ) |s (/) ) ) = x )
94 27 33 93 rspcedvdw 
 |-  ( x e. On -> E. y e. On_s ( ( bday |` On_s ) ` y ) = x )
95 fvelrnb 
 |-  ( ( bday |` On_s ) Fn On_s -> ( x e. ran ( bday |` On_s ) <-> E. y e. On_s ( ( bday |` On_s ) ` y ) = x ) )
96 12 95 ax-mp 
 |-  ( x e. ran ( bday |` On_s ) <-> E. y e. On_s ( ( bday |` On_s ) ` y ) = x )
97 94 96 sylibr 
 |-  ( x e. On -> x e. ran ( bday |` On_s ) )
98 97 ssriv 
 |-  On C_ ran ( bday |` On_s )
99 15 98 eqssi 
 |-  ran ( bday |` On_s ) = On
100 df-fo 
 |-  ( ( bday |` On_s ) : On_s -onto-> On <-> ( ( bday |` On_s ) Fn On_s /\ ran ( bday |` On_s ) = On ) )
101 12 99 100 mpbir2an 
 |-  ( bday |` On_s ) : On_s -onto-> On
102 df-f1o 
 |-  ( ( bday |` On_s ) : On_s -1-1-onto-> On <-> ( ( bday |` On_s ) : On_s -1-1-> On /\ ( bday |` On_s ) : On_s -onto-> On ) )
103 26 101 102 mpbir2an 
 |-  ( bday |` On_s ) : On_s -1-1-onto-> On
104 onslt 
 |-  ( ( x e. On_s /\ y e. On_s ) -> ( x  ( bday ` x ) e. ( bday ` y ) ) )
105 fvex 
 |-  ( bday ` y ) e. _V
106 105 epeli 
 |-  ( ( bday ` x ) _E ( bday ` y ) <-> ( bday ` x ) e. ( bday ` y ) )
107 104 106 bitr4di 
 |-  ( ( x e. On_s /\ y e. On_s ) -> ( x  ( bday ` x ) _E ( bday ` y ) ) )
108 18 19 breqan12d 
 |-  ( ( x e. On_s /\ y e. On_s ) -> ( ( ( bday |` On_s ) ` x ) _E ( ( bday |` On_s ) ` y ) <-> ( bday ` x ) _E ( bday ` y ) ) )
109 107 108 bitr4d 
 |-  ( ( x e. On_s /\ y e. On_s ) -> ( x  ( ( bday |` On_s ) ` x ) _E ( ( bday |` On_s ) ` y ) ) )
110 109 rgen2 
 |-  A. x e. On_s A. y e. On_s ( x  ( ( bday |` On_s ) ` x ) _E ( ( bday |` On_s ) ` y ) )
111 df-isom 
 |-  ( ( bday |` On_s ) Isom  ( ( bday |` On_s ) : On_s -1-1-onto-> On /\ A. x e. On_s A. y e. On_s ( x  ( ( bday |` On_s ) ` x ) _E ( ( bday |` On_s ) ` y ) ) ) )
112 103 110 111 mpbir2an 
 |-  ( bday |` On_s ) Isom