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 ↾ 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		nulssgt	⊢ ( ( 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		scutbdaybnd	⊢ ( ( ( O ‘ 𝑥 ) <<s ∅ ∧ 𝑥 ∈ On ∧ ( bday “ ( ( O ‘ 𝑥 ) ∪ ∅ ) ) ⊆ 𝑥 ) → ( bday ‘ ( ( O ‘ 𝑥 ) |s ∅ ) ) ⊆ 𝑥 )
51	38 39 49 50	mp3an2i	⊢ ( 𝑥 ∈ On → ( bday ‘ ( ( O ‘ 𝑥 ) |s ∅ ) ) ⊆ 𝑥 )
52		ssltsep	⊢ ( ( 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		sltirr	⊢ ( 𝑤 ∈ 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		bdayelon	⊢ ( 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		scutbday	⊢ ( ( 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		onslt	⊢ ( ( 𝑥 ∈ 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 )