Metamath Proof Explorer

Theorem oniso

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 oniso ( bday ↾ Ons ) Isom <s , E ( Ons , On )

Proof

Step Hyp Ref Expression
1 bdayfun ⊢ Fun bday
2 funres ⊢ ( Fun bday → Fun ( bday ↾ Ons ) )
3 1 2 ax-mp ⊢ Fun ( bday ↾ Ons )
4 dmres ⊢ dom ( bday ↾ Ons ) = ( Ons ∩ dom bday )
5 bdaydm ⊢ dom bday = No
6 5 ineq2i ⊢ ( Ons ∩ dom bday ) = ( Ons ∩ No )
7 onssno ⊢ Ons ⊆ No
8 dfss2 ⊢ ( Ons ⊆ No ↔ ( Ons ∩ No ) = Ons )
9 7 8 mpbi ⊢ ( Ons ∩ No ) = Ons
10 4 6 9 3eqtri ⊢ dom ( bday ↾ Ons ) = Ons
11 df-fn ⊢ ( ( bday ↾ Ons ) Fn Ons ↔ ( Fun ( bday ↾ Ons ) ∧ dom ( bday ↾ Ons ) = Ons ) )
12 3 10 11 mpbir2an ⊢ ( bday ↾ Ons ) Fn Ons
13 rnresss ⊢ ran ( bday ↾ Ons ) ⊆ ran bday
14 bdayrn ⊢ ran bday = On
15 13 14 sseqtri ⊢ ran ( bday ↾ Ons ) ⊆ On
16 df-f ⊢ ( ( bday ↾ Ons ) : Ons ⟶ On ↔ ( ( bday ↾ Ons ) Fn Ons ∧ ran ( bday ↾ Ons ) ⊆ On ) )
17 12 15 16 mpbir2an ⊢ ( bday ↾ Ons ) : Ons ⟶ On
18 fvres ⊢ ( 𝑥 ∈ Ons → ( ( bday ↾ Ons ) ‘ 𝑥 ) = ( bday ‘ 𝑥 ) )
19 fvres ⊢ ( 𝑦 ∈ Ons → ( ( bday ↾ Ons ) ‘ 𝑦 ) = ( bday ‘ 𝑦 ) )
20 18 19 eqeqan12d ⊢ ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) → ( ( ( bday ↾ Ons ) ‘ 𝑥 ) = ( ( bday ↾ Ons ) ‘ 𝑦 ) ↔ ( bday ‘ 𝑥 ) = ( bday ‘ 𝑦 ) ) )
21 bday11on ⊢ ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ∧ ( bday ‘ 𝑥 ) = ( bday ‘ 𝑦 ) ) → 𝑥 = 𝑦 )
22 21 3expia ⊢ ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) → ( ( bday ‘ 𝑥 ) = ( bday ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
23 20 22 sylbid ⊢ ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) → ( ( ( bday ↾ Ons ) ‘ 𝑥 ) = ( ( bday ↾ Ons ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
24 23 rgen2 ⊢ ∀ 𝑥 ∈ Ons ∀ 𝑦 ∈ Ons ( ( ( bday ↾ Ons ) ‘ 𝑥 ) = ( ( bday ↾ Ons ) ‘ 𝑦 ) → 𝑥 = 𝑦 )
25 dff13 ⊢ ( ( bday ↾ Ons ) : Ons –1-1→ On ↔ ( ( bday ↾ Ons ) : Ons ⟶ On ∧ ∀ 𝑥 ∈ Ons ∀ 𝑦 ∈ Ons ( ( ( bday ↾ Ons ) ‘ 𝑥 ) = ( ( bday ↾ Ons ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
26 17 24 25 mpbir2an ⊢ ( bday ↾ Ons ) : Ons –1-1→ On
27 fveqeq2 ⊢ ( 𝑦 = ( ( O ‘ 𝑥 ) |s ∅ ) → ( ( ( bday ↾ Ons ) ‘ 𝑦 ) = 𝑥 ↔ ( ( bday ↾ Ons ) ‘ ( ( O ‘ 𝑥 ) |s ∅ ) ) = 𝑥 ) )
28 fvex ⊢ ( O ‘ 𝑥 ) ∈ V
29 28 a1i ⊢ ( 𝑥 ∈ On → ( O ‘ 𝑥 ) ∈ V )
30 oldssno ⊢ ( O ‘ 𝑥 ) ⊆ No
31 30 a1i ⊢ ( 𝑥 ∈ On → ( O ‘ 𝑥 ) ⊆ No )
32 eqidd ⊢ ( 𝑥 ∈ On → ( ( O ‘ 𝑥 ) |s ∅ ) = ( ( O ‘ 𝑥 ) |s ∅ ) )
33 29 31 32 elons2d ⊢ ( 𝑥 ∈ On → ( ( O ‘ 𝑥 ) |s ∅ ) ∈ Ons )
34 33 fvresd ⊢ ( 𝑥 ∈ On → ( ( bday ↾ Ons ) ‘ ( ( O ‘ 𝑥 ) |s ∅ ) ) = ( bday ‘ ( ( O ‘ 𝑥 ) |s ∅ ) ) )
35 28 elpw ⊢ ( ( O ‘ 𝑥 ) ∈ 𝒫 No ↔ ( O ‘ 𝑥 ) ⊆ No )
36 30 35 mpbir ⊢ ( O ‘ 𝑥 ) ∈ 𝒫 No
37 nulsgts ⊢ ( ( O ‘ 𝑥 ) ∈ 𝒫 No → ( O ‘ 𝑥 ) <<s ∅ )
38 36 37 ax-mp ⊢ ( O ‘ 𝑥 ) <<s ∅
39 id ⊢ ( 𝑥 ∈ On → 𝑥 ∈ On )
40 un0 ⊢ ( ( O ‘ 𝑥 ) ∪ ∅ ) = ( O ‘ 𝑥 )
41 40 imaeq2i ⊢ ( bday “ ( ( O ‘ 𝑥 ) ∪ ∅ ) ) = ( bday “ ( O ‘ 𝑥 ) )
42 oldbdayim ⊢ ( 𝑦 ∈ ( O ‘ 𝑥 ) → ( bday ‘ 𝑦 ) ∈ 𝑥 )
43 42 rgen ⊢ ∀ 𝑦 ∈ ( O ‘ 𝑥 ) ( bday ‘ 𝑦 ) ∈ 𝑥
44 43 a1i ⊢ ( 𝑥 ∈ On → ∀ 𝑦 ∈ ( O ‘ 𝑥 ) ( bday ‘ 𝑦 ) ∈ 𝑥 )
45 30 5 sseqtrri ⊢ ( O ‘ 𝑥 ) ⊆ dom bday
46 funimass4 ⊢ ( ( Fun bday ∧ ( O ‘ 𝑥 ) ⊆ dom bday ) → ( ( bday “ ( O ‘ 𝑥 ) ) ⊆ 𝑥 ↔ ∀ 𝑦 ∈ ( O ‘ 𝑥 ) ( bday ‘ 𝑦 ) ∈ 𝑥 ) )
47 1 45 46 mp2an ⊢ ( ( bday “ ( O ‘ 𝑥 ) ) ⊆ 𝑥 ↔ ∀ 𝑦 ∈ ( O ‘ 𝑥 ) ( bday ‘ 𝑦 ) ∈ 𝑥 )
48 44 47 sylibr ⊢ ( 𝑥 ∈ On → ( bday “ ( O ‘ 𝑥 ) ) ⊆ 𝑥 )
49 41 48 eqsstrid ⊢ ( 𝑥 ∈ On → ( bday “ ( ( O ‘ 𝑥 ) ∪ ∅ ) ) ⊆ 𝑥 )
50 cutbdaybnd ⊢ ( ( ( O ‘ 𝑥 ) <<s ∅ ∧ 𝑥 ∈ On ∧ ( bday “ ( ( O ‘ 𝑥 ) ∪ ∅ ) ) ⊆ 𝑥 ) → ( bday ‘ ( ( O ‘ 𝑥 ) |s ∅ ) ) ⊆ 𝑥 )
51 38 39 49 50 mp3an2i ⊢ ( 𝑥 ∈ On → ( bday ‘ ( ( O ‘ 𝑥 ) |s ∅ ) ) ⊆ 𝑥 )
52 sltssep ⊢ ( ( O ‘ 𝑥 ) <<s { 𝑤 } → ∀ 𝑦 ∈ ( O ‘ 𝑥 ) ∀ 𝑧 ∈ { 𝑤 } 𝑦 <s 𝑧 )
53 vex ⊢ 𝑤 ∈ V
54 breq2 ⊢ ( 𝑧 = 𝑤 → ( 𝑦 <s 𝑧 ↔ 𝑦 <s 𝑤 ) )
55 53 54 ralsn ⊢ ( ∀ 𝑧 ∈ { 𝑤 } 𝑦 <s 𝑧 ↔ 𝑦 <s 𝑤 )
56 55 ralbii ⊢ ( ∀ 𝑦 ∈ ( O ‘ 𝑥 ) ∀ 𝑧 ∈ { 𝑤 } 𝑦 <s 𝑧 ↔ ∀ 𝑦 ∈ ( O ‘ 𝑥 ) 𝑦 <s 𝑤 )
57 52 56 sylib ⊢ ( ( O ‘ 𝑥 ) <<s { 𝑤 } → ∀ 𝑦 ∈ ( O ‘ 𝑥 ) 𝑦 <s 𝑤 )
58 ltsirr ⊢ ( 𝑤 ∈ No → ¬ 𝑤 <s 𝑤 )
59 58 3ad2ant2 ⊢ ( ( 𝑥 ∈ On ∧ 𝑤 ∈ No ∧ ∀ 𝑦 ∈ ( O ‘ 𝑥 ) 𝑦 <s 𝑤 ) → ¬ 𝑤 <s 𝑤 )
60 oldbday ⊢ ( ( 𝑥 ∈ On ∧ 𝑤 ∈ No ) → ( 𝑤 ∈ ( O ‘ 𝑥 ) ↔ ( bday ‘ 𝑤 ) ∈ 𝑥 ) )
61 60 3adant3 ⊢ ( ( 𝑥 ∈ On ∧ 𝑤 ∈ No ∧ ∀ 𝑦 ∈ ( O ‘ 𝑥 ) 𝑦 <s 𝑤 ) → ( 𝑤 ∈ ( O ‘ 𝑥 ) ↔ ( bday ‘ 𝑤 ) ∈ 𝑥 ) )
62 breq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 <s 𝑤 ↔ 𝑤 <s 𝑤 ) )
63 62 rspccv ⊢ ( ∀ 𝑦 ∈ ( O ‘ 𝑥 ) 𝑦 <s 𝑤 → ( 𝑤 ∈ ( O ‘ 𝑥 ) → 𝑤 <s 𝑤 ) )
64 63 3ad2ant3 ⊢ ( ( 𝑥 ∈ On ∧ 𝑤 ∈ No ∧ ∀ 𝑦 ∈ ( O ‘ 𝑥 ) 𝑦 <s 𝑤 ) → ( 𝑤 ∈ ( O ‘ 𝑥 ) → 𝑤 <s 𝑤 ) )
65 61 64 sylbird ⊢ ( ( 𝑥 ∈ On ∧ 𝑤 ∈ No ∧ ∀ 𝑦 ∈ ( O ‘ 𝑥 ) 𝑦 <s 𝑤 ) → ( ( bday ‘ 𝑤 ) ∈ 𝑥 → 𝑤 <s 𝑤 ) )
66 59 65 mtod ⊢ ( ( 𝑥 ∈ On ∧ 𝑤 ∈ No ∧ ∀ 𝑦 ∈ ( O ‘ 𝑥 ) 𝑦 <s 𝑤 ) → ¬ ( bday ‘ 𝑤 ) ∈ 𝑥 )
67 simp1 ⊢ ( ( 𝑥 ∈ On ∧ 𝑤 ∈ No ∧ ∀ 𝑦 ∈ ( O ‘ 𝑥 ) 𝑦 <s 𝑤 ) → 𝑥 ∈ On )
68 bdayon ⊢ ( bday ‘ 𝑤 ) ∈ On
69 ontri1 ⊢ ( ( 𝑥 ∈ On ∧ ( bday ‘ 𝑤 ) ∈ On ) → ( 𝑥 ⊆ ( bday ‘ 𝑤 ) ↔ ¬ ( bday ‘ 𝑤 ) ∈ 𝑥 ) )
70 67 68 69 sylancl ⊢ ( ( 𝑥 ∈ On ∧ 𝑤 ∈ No ∧ ∀ 𝑦 ∈ ( O ‘ 𝑥 ) 𝑦 <s 𝑤 ) → ( 𝑥 ⊆ ( bday ‘ 𝑤 ) ↔ ¬ ( bday ‘ 𝑤 ) ∈ 𝑥 ) )
71 66 70 mpbird ⊢ ( ( 𝑥 ∈ On ∧ 𝑤 ∈ No ∧ ∀ 𝑦 ∈ ( O ‘ 𝑥 ) 𝑦 <s 𝑤 ) → 𝑥 ⊆ ( bday ‘ 𝑤 ) )
72 71 3expia ⊢ ( ( 𝑥 ∈ On ∧ 𝑤 ∈ No ) → ( ∀ 𝑦 ∈ ( O ‘ 𝑥 ) 𝑦 <s 𝑤 → 𝑥 ⊆ ( bday ‘ 𝑤 ) ) )
73 57 72 syl5 ⊢ ( ( 𝑥 ∈ On ∧ 𝑤 ∈ No ) → ( ( O ‘ 𝑥 ) <<s { 𝑤 } → 𝑥 ⊆ ( bday ‘ 𝑤 ) ) )
74 73 adantrd ⊢ ( ( 𝑥 ∈ On ∧ 𝑤 ∈ No ) → ( ( ( O ‘ 𝑥 ) <<s { 𝑤 } ∧ { 𝑤 } <<s ∅ ) → 𝑥 ⊆ ( bday ‘ 𝑤 ) ) )
75 74 ralrimiva ⊢ ( 𝑥 ∈ On → ∀ 𝑤 ∈ No ( ( ( O ‘ 𝑥 ) <<s { 𝑤 } ∧ { 𝑤 } <<s ∅ ) → 𝑥 ⊆ ( bday ‘ 𝑤 ) ) )
76 ssint ⊢ ( 𝑥 ⊆ ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( O ‘ 𝑥 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) } ) ↔ ∀ 𝑧 ∈ ( bday “ { 𝑦 ∈ No ∣ ( ( O ‘ 𝑥 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) } ) 𝑥 ⊆ 𝑧 )
77 bdayfn ⊢ bday Fn No
78 ssrab2 ⊢ { 𝑦 ∈ No ∣ ( ( O ‘ 𝑥 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) } ⊆ No
79 sseq2 ⊢ ( 𝑧 = ( bday ‘ 𝑤 ) → ( 𝑥 ⊆ 𝑧 ↔ 𝑥 ⊆ ( bday ‘ 𝑤 ) ) )
80 79 ralima ⊢ ( ( bday Fn No ∧ { 𝑦 ∈ No ∣ ( ( O ‘ 𝑥 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) } ⊆ No ) → ( ∀ 𝑧 ∈ ( bday “ { 𝑦 ∈ No ∣ ( ( O ‘ 𝑥 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) } ) 𝑥 ⊆ 𝑧 ↔ ∀ 𝑤 ∈ { 𝑦 ∈ No ∣ ( ( O ‘ 𝑥 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) } 𝑥 ⊆ ( bday ‘ 𝑤 ) ) )
81 77 78 80 mp2an ⊢ ( ∀ 𝑧 ∈ ( bday “ { 𝑦 ∈ No ∣ ( ( O ‘ 𝑥 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) } ) 𝑥 ⊆ 𝑧 ↔ ∀ 𝑤 ∈ { 𝑦 ∈ No ∣ ( ( O ‘ 𝑥 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) } 𝑥 ⊆ ( bday ‘ 𝑤 ) )
82 sneq ⊢ ( 𝑦 = 𝑤 → { 𝑦 } = { 𝑤 } )
83 82 breq2d ⊢ ( 𝑦 = 𝑤 → ( ( O ‘ 𝑥 ) <<s { 𝑦 } ↔ ( O ‘ 𝑥 ) <<s { 𝑤 } ) )
84 82 breq1d ⊢ ( 𝑦 = 𝑤 → ( { 𝑦 } <<s ∅ ↔ { 𝑤 } <<s ∅ ) )
85 83 84 anbi12d ⊢ ( 𝑦 = 𝑤 → ( ( ( O ‘ 𝑥 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) ↔ ( ( O ‘ 𝑥 ) <<s { 𝑤 } ∧ { 𝑤 } <<s ∅ ) ) )
86 85 ralrab ⊢ ( ∀ 𝑤 ∈ { 𝑦 ∈ No ∣ ( ( O ‘ 𝑥 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) } 𝑥 ⊆ ( bday ‘ 𝑤 ) ↔ ∀ 𝑤 ∈ No ( ( ( O ‘ 𝑥 ) <<s { 𝑤 } ∧ { 𝑤 } <<s ∅ ) → 𝑥 ⊆ ( bday ‘ 𝑤 ) ) )
87 76 81 86 3bitri ⊢ ( 𝑥 ⊆ ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( O ‘ 𝑥 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) } ) ↔ ∀ 𝑤 ∈ No ( ( ( O ‘ 𝑥 ) <<s { 𝑤 } ∧ { 𝑤 } <<s ∅ ) → 𝑥 ⊆ ( bday ‘ 𝑤 ) ) )
88 75 87 sylibr ⊢ ( 𝑥 ∈ On → 𝑥 ⊆ ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( O ‘ 𝑥 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) } ) )
89 cutbday ⊢ ( ( O ‘ 𝑥 ) <<s ∅ → ( bday ‘ ( ( O ‘ 𝑥 ) |s ∅ ) ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( O ‘ 𝑥 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) } ) )
90 38 89 ax-mp ⊢ ( bday ‘ ( ( O ‘ 𝑥 ) |s ∅ ) ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( ( O ‘ 𝑥 ) <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) } )
91 88 90 sseqtrrdi ⊢ ( 𝑥 ∈ On → 𝑥 ⊆ ( bday ‘ ( ( O ‘ 𝑥 ) |s ∅ ) ) )
92 51 91 eqssd ⊢ ( 𝑥 ∈ On → ( bday ‘ ( ( O ‘ 𝑥 ) |s ∅ ) ) = 𝑥 )
93 34 92 eqtrd ⊢ ( 𝑥 ∈ On → ( ( bday ↾ Ons ) ‘ ( ( O ‘ 𝑥 ) |s ∅ ) ) = 𝑥 )
94 27 33 93 rspcedvdw ⊢ ( 𝑥 ∈ On → ∃ 𝑦 ∈ Ons ( ( bday ↾ Ons ) ‘ 𝑦 ) = 𝑥 )
95 fvelrnb ⊢ ( ( bday ↾ Ons ) Fn Ons → ( 𝑥 ∈ ran ( bday ↾ Ons ) ↔ ∃ 𝑦 ∈ Ons ( ( bday ↾ Ons ) ‘ 𝑦 ) = 𝑥 ) )
96 12 95 ax-mp ⊢ ( 𝑥 ∈ ran ( bday ↾ Ons ) ↔ ∃ 𝑦 ∈ Ons ( ( bday ↾ Ons ) ‘ 𝑦 ) = 𝑥 )
97 94 96 sylibr ⊢ ( 𝑥 ∈ On → 𝑥 ∈ ran ( bday ↾ Ons ) )
98 97 ssriv ⊢ On ⊆ ran ( bday ↾ Ons )
99 15 98 eqssi ⊢ ran ( bday ↾ Ons ) = On
100 df-fo ⊢ ( ( bday ↾ Ons ) : Ons –onto→ On ↔ ( ( bday ↾ Ons ) Fn Ons ∧ ran ( bday ↾ Ons ) = On ) )
101 12 99 100 mpbir2an ⊢ ( bday ↾ Ons ) : Ons –onto→ On
102 df-f1o ⊢ ( ( bday ↾ Ons ) : Ons –1-1-onto→ On ↔ ( ( bday ↾ Ons ) : Ons –1-1→ On ∧ ( bday ↾ Ons ) : Ons –onto→ On ) )
103 26 101 102 mpbir2an ⊢ ( bday ↾ Ons ) : Ons –1-1-onto→ On
104 onlts ⊢ ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) → ( 𝑥 <s 𝑦 ↔ ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝑦 ) ) )
105 fvex ⊢ ( bday ‘ 𝑦 ) ∈ V
106 105 epeli ⊢ ( ( bday ‘ 𝑥 ) E ( bday ‘ 𝑦 ) ↔ ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝑦 ) )
107 104 106 bitr4di ⊢ ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) → ( 𝑥 <s 𝑦 ↔ ( bday ‘ 𝑥 ) E ( bday ‘ 𝑦 ) ) )
108 18 19 breqan12d ⊢ ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) → ( ( ( bday ↾ Ons ) ‘ 𝑥 ) E ( ( bday ↾ Ons ) ‘ 𝑦 ) ↔ ( bday ‘ 𝑥 ) E ( bday ‘ 𝑦 ) ) )
109 107 108 bitr4d ⊢ ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) → ( 𝑥 <s 𝑦 ↔ ( ( bday ↾ Ons ) ‘ 𝑥 ) E ( ( bday ↾ Ons ) ‘ 𝑦 ) ) )
110 109 rgen2 ⊢ ∀ 𝑥 ∈ Ons ∀ 𝑦 ∈ Ons ( 𝑥 <s 𝑦 ↔ ( ( bday ↾ Ons ) ‘ 𝑥 ) E ( ( bday ↾ Ons ) ‘ 𝑦 ) )
111 df-isom ⊢ ( ( bday ↾ Ons ) Isom <s , E ( Ons , On ) ↔ ( ( bday ↾ Ons ) : Ons –1-1-onto→ On ∧ ∀ 𝑥 ∈ Ons ∀ 𝑦 ∈ Ons ( 𝑥 <s 𝑦 ↔ ( ( bday ↾ Ons ) ‘ 𝑥 ) E ( ( bday ↾ Ons ) ‘ 𝑦 ) ) ) )
112 103 110 111 mpbir2an ⊢ ( bday ↾ Ons ) Isom <s , E ( Ons , On )