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 ↾}_{{On}_{s}}) {Isom}_{<_{s}, E} ({On}_{s}, On)$

Proof

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

Metamath Proof Explorer

Theorem oniso

Proof