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	$$⊢\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right):{\mathbb{N}}_{\mathrm{0s}}\underset{1-1\; onto}{⟶}\mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		bdayfun	$$⊢\mathrm{Fun}\mathrm{bday}$$
2		funres	$$⊢\mathrm{Fun}\mathrm{bday}\to \mathrm{Fun}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)$$
3	1 2	ax-mp	$$⊢\mathrm{Fun}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)$$
4		dmres	$$⊢\mathrm{dom}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)={\mathbb{N}}_{\mathrm{0s}}\cap \mathrm{dom}\mathrm{bday}$$
5		bdaydm	$$⊢\mathrm{dom}\mathrm{bday}=\mathrm{No}$$
6	5	ineq2i	$$⊢{\mathbb{N}}_{\mathrm{0s}}\cap \mathrm{dom}\mathrm{bday}={\mathbb{N}}_{\mathrm{0s}}\cap \mathrm{No}$$
7		n0ssno	$$⊢{\mathbb{N}}_{\mathrm{0s}}\subseteq \mathrm{No}$$
8		dfss2	$$⊢{\mathbb{N}}_{\mathrm{0s}}\subseteq \mathrm{No}\leftrightarrow {\mathbb{N}}_{\mathrm{0s}}\cap \mathrm{No}={\mathbb{N}}_{\mathrm{0s}}$$
9	7 8	mpbi	$$⊢{\mathbb{N}}_{\mathrm{0s}}\cap \mathrm{No}={\mathbb{N}}_{\mathrm{0s}}$$
10	4 6 9	3eqtri	$$⊢\mathrm{dom}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)={\mathbb{N}}_{\mathrm{0s}}$$
11		df-fn	$$⊢\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)Fn{\mathbb{N}}_{\mathrm{0s}}\leftrightarrow \left(\mathrm{Fun}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\wedge \mathrm{dom}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)={\mathbb{N}}_{\mathrm{0s}}\right)$$
12	3 10 11	mpbir2an	$$⊢\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)Fn{\mathbb{N}}_{\mathrm{0s}}$$
13		fvres	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to \left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left(x\right)=\mathrm{bday}\left(x\right)$$
14		n0sbday	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to \mathrm{bday}\left(x\right)\in \mathrm{\omega }$$
15	13 14	eqeltrd	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to \left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left(x\right)\in \mathrm{\omega }$$
16	15	rgen	$$⊢\forall x\in {\mathbb{N}}_{\mathrm{0s}}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left(x\right)\in \mathrm{\omega }$$
17		fnfvrnss	$$⊢\left(\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)Fn{\mathbb{N}}_{\mathrm{0s}}\wedge \forall x\in {\mathbb{N}}_{\mathrm{0s}}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left(x\right)\in \mathrm{\omega }\right)\to \mathrm{ran}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\subseteq \mathrm{\omega }$$
18	12 16 17	mp2an	$$⊢\mathrm{ran}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\subseteq \mathrm{\omega }$$
19		eqeq2	$$⊢b=\varnothing \to \left(\mathrm{bday}\left(y\right)=b\leftrightarrow \mathrm{bday}\left(y\right)=\varnothing \right)$$
20	19	rexbidv	$$⊢b=\varnothing \to \left(\exists y\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(y\right)=b\leftrightarrow \exists y\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(y\right)=\varnothing \right)$$
21		eqeq2	$$⊢b=a\to \left(\mathrm{bday}\left(y\right)=b\leftrightarrow \mathrm{bday}\left(y\right)=a\right)$$
22	21	rexbidv	$$⊢b=a\to \left(\exists y\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(y\right)=b\leftrightarrow \exists y\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(y\right)=a\right)$$
23		eqeq2	$$⊢b=\mathrm{suc}a\to \left(\mathrm{bday}\left(y\right)=b\leftrightarrow \mathrm{bday}\left(y\right)=\mathrm{suc}a\right)$$
24	23	rexbidv	$$⊢b=\mathrm{suc}a\to \left(\exists y\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(y\right)=b\leftrightarrow \exists y\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(y\right)=\mathrm{suc}a\right)$$
25		fveqeq2	$$⊢y=z\to \left(\mathrm{bday}\left(y\right)=\mathrm{suc}a\leftrightarrow \mathrm{bday}\left(z\right)=\mathrm{suc}a\right)$$
26	25	cbvrexvw	$$⊢\exists y\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(y\right)=\mathrm{suc}a\leftrightarrow \exists z\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(z\right)=\mathrm{suc}a$$
27	24 26	bitrdi	$$⊢b=\mathrm{suc}a\to \left(\exists y\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(y\right)=b\leftrightarrow \exists z\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(z\right)=\mathrm{suc}a\right)$$
28		eqeq2	$$⊢b=x\to \left(\mathrm{bday}\left(y\right)=b\leftrightarrow \mathrm{bday}\left(y\right)=x\right)$$
29	28	rexbidv	$$⊢b=x\to \left(\exists y\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(y\right)=b\leftrightarrow \exists y\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(y\right)=x\right)$$
30		0n0s	$$⊢0_s\in {\mathbb{N}}_{\mathrm{0s}}$$
31		bday0s	$$⊢\mathrm{bday}\left(0_s\right)=\varnothing$$
32		fveqeq2	$$⊢y=0_s\to \left(\mathrm{bday}\left(y\right)=\varnothing \leftrightarrow \mathrm{bday}\left(0_s\right)=\varnothing \right)$$
33	32	rspcev	$$⊢\left(0_s\in {\mathbb{N}}_{\mathrm{0s}}\wedge \mathrm{bday}\left(0_s\right)=\varnothing \right)\to \exists y\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(y\right)=\varnothing$$
34	30 31 33	mp2an	$$⊢\exists y\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(y\right)=\varnothing$$
35		fveqeq2	$$⊢z=y{+}_s{1}_s\to \left(\mathrm{bday}\left(z\right)=\mathrm{suc}\mathrm{bday}\left(y\right)\leftrightarrow \mathrm{bday}\left(y{+}_s{1}_s\right)=\mathrm{suc}\mathrm{bday}\left(y\right)\right)$$
36		peano2n0s	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to y{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
37		bdayn0p1	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to \mathrm{bday}\left(y{+}_s{1}_s\right)=\mathrm{suc}\mathrm{bday}\left(y\right)$$
38	35 36 37	rspcedvdw	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to \exists z\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(z\right)=\mathrm{suc}\mathrm{bday}\left(y\right)$$
39	38	adantl	$$⊢\left(a\in \mathrm{\omega }\wedge y\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \exists z\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(z\right)=\mathrm{suc}\mathrm{bday}\left(y\right)$$
40		suceq	$$⊢\mathrm{bday}\left(y\right)=a\to \mathrm{suc}\mathrm{bday}\left(y\right)=\mathrm{suc}a$$
41	40	eqeq2d	$$⊢\mathrm{bday}\left(y\right)=a\to \left(\mathrm{bday}\left(z\right)=\mathrm{suc}\mathrm{bday}\left(y\right)\leftrightarrow \mathrm{bday}\left(z\right)=\mathrm{suc}a\right)$$
42	41	rexbidv	$$⊢\mathrm{bday}\left(y\right)=a\to \left(\exists z\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(z\right)=\mathrm{suc}\mathrm{bday}\left(y\right)\leftrightarrow \exists z\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(z\right)=\mathrm{suc}a\right)$$
43	39 42	syl5ibcom	$$⊢\left(a\in \mathrm{\omega }\wedge y\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(\mathrm{bday}\left(y\right)=a\to \exists z\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(z\right)=\mathrm{suc}a\right)$$
44	43	rexlimdva	$$⊢a\in \mathrm{\omega }\to \left(\exists y\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(y\right)=a\to \exists z\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(z\right)=\mathrm{suc}a\right)$$
45	20 22 27 29 34 44	finds	$$⊢x\in \mathrm{\omega }\to \exists y\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(y\right)=x$$
46		fvelrnb	$$⊢\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)Fn{\mathbb{N}}_{\mathrm{0s}}\to \left(x\in \mathrm{ran}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\leftrightarrow \exists y\in {\mathbb{N}}_{\mathrm{0s}}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left(y\right)=x\right)$$
47	12 46	ax-mp	$$⊢x\in \mathrm{ran}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\leftrightarrow \exists y\in {\mathbb{N}}_{\mathrm{0s}}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left(y\right)=x$$
48		fvres	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to \left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left(y\right)=\mathrm{bday}\left(y\right)$$
49	48	eqeq1d	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to \left(\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left(y\right)=x\leftrightarrow \mathrm{bday}\left(y\right)=x\right)$$
50	49	rexbiia	$$⊢\exists y\in {\mathbb{N}}_{\mathrm{0s}}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left(y\right)=x\leftrightarrow \exists y\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(y\right)=x$$
51	47 50	bitri	$$⊢x\in \mathrm{ran}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\leftrightarrow \exists y\in {\mathbb{N}}_{\mathrm{0s}}\mathrm{bday}\left(y\right)=x$$
52	45 51	sylibr	$$⊢x\in \mathrm{\omega }\to x\in \mathrm{ran}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)$$
53	52	ssriv	$$⊢\mathrm{\omega }\subseteq \mathrm{ran}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)$$
54	18 53	eqssi	$$⊢\mathrm{ran}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)=\mathrm{\omega }$$
55		df-fo	$$⊢\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right):{\mathbb{N}}_{\mathrm{0s}}\underset{onto}{⟶}\mathrm{\omega }\leftrightarrow \left(\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)Fn{\mathbb{N}}_{\mathrm{0s}}\wedge \mathrm{ran}\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)=\mathrm{\omega }\right)$$
56	12 54 55	mpbir2an	$$⊢\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right):{\mathbb{N}}_{\mathrm{0s}}\underset{onto}{⟶}\mathrm{\omega }$$
57		fof	$$⊢\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right):{\mathbb{N}}_{\mathrm{0s}}\underset{onto}{⟶}\mathrm{\omega }\to \left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right):{\mathbb{N}}_{\mathrm{0s}}⟶\mathrm{\omega }$$
58	56 57	ax-mp	$$⊢\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right):{\mathbb{N}}_{\mathrm{0s}}⟶\mathrm{\omega }$$
59	13 48	eqeqan12d	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge y\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left(x\right)=\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left(y\right)\leftrightarrow \mathrm{bday}\left(x\right)=\mathrm{bday}\left(y\right)\right)$$
60		n0ons	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to x\in {On}_s$$
61		n0ons	$$⊢y\in {\mathbb{N}}_{\mathrm{0s}}\to y\in {On}_s$$
62		bday11on	$$⊢\left(x\in {On}_s\wedge y\in {On}_s\wedge \mathrm{bday}\left(x\right)=\mathrm{bday}\left(y\right)\right)\to x=y$$
63	62	3expia	$$⊢\left(x\in {On}_s\wedge y\in {On}_s\right)\to \left(\mathrm{bday}\left(x\right)=\mathrm{bday}\left(y\right)\to x=y\right)$$
64	60 61 63	syl2an	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge y\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(\mathrm{bday}\left(x\right)=\mathrm{bday}\left(y\right)\to x=y\right)$$
65	59 64	sylbid	$$⊢\left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge y\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \left(\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left(x\right)=\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left(y\right)\to x=y\right)$$
66	65	rgen2	$$⊢\forall x\in {\mathbb{N}}_{\mathrm{0s}}\forall y\in {\mathbb{N}}_{\mathrm{0s}}\left(\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left(x\right)=\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left(y\right)\to x=y\right)$$
67		dff13	$$⊢\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right):{\mathbb{N}}_{\mathrm{0s}}\underset{1-1}{⟶}\mathrm{\omega }\leftrightarrow \left(\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right):{\mathbb{N}}_{\mathrm{0s}}⟶\mathrm{\omega }\wedge \forall x\in {\mathbb{N}}_{\mathrm{0s}}\forall y\in {\mathbb{N}}_{\mathrm{0s}}\left(\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left(x\right)=\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right)\left(y\right)\to x=y\right)\right)$$
68	58 66 67	mpbir2an	$$⊢\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right):{\mathbb{N}}_{\mathrm{0s}}\underset{1-1}{⟶}\mathrm{\omega }$$
69		df-f1o	$$⊢\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right):{\mathbb{N}}_{\mathrm{0s}}\underset{1-1\; onto}{⟶}\mathrm{\omega }\leftrightarrow \left(\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right):{\mathbb{N}}_{\mathrm{0s}}\underset{1-1}{⟶}\mathrm{\omega }\wedge \left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right):{\mathbb{N}}_{\mathrm{0s}}\underset{onto}{⟶}\mathrm{\omega }\right)$$
70	68 56 69	mpbir2an	$$⊢\left({\mathrm{bday}\upharpoonright }_{{\mathbb{N}}_{\mathrm{0s}}}\right):{\mathbb{N}}_{\mathrm{0s}}\underset{1-1\; onto}{⟶}\mathrm{\omega }$$