Theorem zsbday

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

	Ref	Expression
Assertion	zsbday	⊢ ( 𝐴 ∈ ℤs → ( bday ‘ 𝐴 ) ∈ ω )

Proof

Step	Hyp	Ref	Expression
1		elzn0s	⊢ ( 𝐴 ∈ ℤs ↔ ( 𝐴 ∈ No ∧ ( 𝐴 ∈ ℕ0s ∨ ( -us ‘ 𝐴 ) ∈ ℕ0s ) ) )
2		n0sbday	⊢ ( 𝐴 ∈ ℕ0s → ( bday ‘ 𝐴 ) ∈ ω )
3	2	adantl	⊢ ( ( 𝐴 ∈ No ∧ 𝐴 ∈ ℕ0s ) → ( bday ‘ 𝐴 ) ∈ ω )
4		negsbday	⊢ ( 𝐴 ∈ No → ( bday ‘ ( -us ‘ 𝐴 ) ) = ( bday ‘ 𝐴 ) )
5	4	adantr	⊢ ( ( 𝐴 ∈ No ∧ ( -us ‘ 𝐴 ) ∈ ℕ0s ) → ( bday ‘ ( -us ‘ 𝐴 ) ) = ( bday ‘ 𝐴 ) )
6		n0sbday	⊢ ( ( -us ‘ 𝐴 ) ∈ ℕ0s → ( bday ‘ ( -us ‘ 𝐴 ) ) ∈ ω )
7	6	adantl	⊢ ( ( 𝐴 ∈ No ∧ ( -us ‘ 𝐴 ) ∈ ℕ0s ) → ( bday ‘ ( -us ‘ 𝐴 ) ) ∈ ω )
8	5 7	eqeltrrd	⊢ ( ( 𝐴 ∈ No ∧ ( -us ‘ 𝐴 ) ∈ ℕ0s ) → ( bday ‘ 𝐴 ) ∈ ω )
9	3 8	jaodan	⊢ ( ( 𝐴 ∈ No ∧ ( 𝐴 ∈ ℕ0s ∨ ( -us ‘ 𝐴 ) ∈ ℕ0s ) ) → ( bday ‘ 𝐴 ) ∈ ω )
10	1 9	sylbi	⊢ ( 𝐴 ∈ ℤs → ( bday ‘ 𝐴 ) ∈ ω )