Theorem zsbday

Description: A surreal integer has a finite birthday. (Contributed by Scott Fenton, 26-May-2025)

	Ref	Expression
Assertion	zsbday	$$⊢A\in {\mathbb{Z}}_s\to \mathrm{bday}\left(A\right)\in \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		elzn0s	$$⊢A\in {\mathbb{Z}}_s\leftrightarrow \left(A\in \mathrm{No}\wedge \left(A\in {\mathbb{N}}_{\mathrm{0s}}\vee {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
2		n0sbday	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \mathrm{bday}\left(A\right)\in \mathrm{\omega }$$
3	2	adantl	$$⊢\left(A\in \mathrm{No}\wedge A\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \mathrm{bday}\left(A\right)\in \mathrm{\omega }$$
4		negsbday	$$⊢A\in \mathrm{No}\to \mathrm{bday}\left({+}_s\left(A\right)\right)=\mathrm{bday}\left(A\right)$$
5	4	adantr	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \mathrm{bday}\left({+}_s\left(A\right)\right)=\mathrm{bday}\left(A\right)$$
6		n0sbday	$$⊢{+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\to \mathrm{bday}\left({+}_s\left(A\right)\right)\in \mathrm{\omega }$$
7	6	adantl	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \mathrm{bday}\left({+}_s\left(A\right)\right)\in \mathrm{\omega }$$
8	5 7	eqeltrrd	$$⊢\left(A\in \mathrm{No}\wedge {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\to \mathrm{bday}\left(A\right)\in \mathrm{\omega }$$
9	3 8	jaodan	$$⊢\left(A\in \mathrm{No}\wedge \left(A\in {\mathbb{N}}_{\mathrm{0s}}\vee {+}_s\left(A\right)\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)\to \mathrm{bday}\left(A\right)\in \mathrm{\omega }$$
10	1 9	sylbi	$$⊢A\in {\mathbb{Z}}_s\to \mathrm{bday}\left(A\right)\in \mathrm{\omega }$$