Metamath Proof Explorer

Theorem zsbday

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

Ref Expression
Assertion zsbday 
|- ( A e. ZZ_s -> ( bday ` A ) e. _om )

Proof

Step Hyp Ref Expression
1 elzn0s 
 |-  ( A e. ZZ_s <-> ( A e. No /\ ( A e. NN0_s \/ ( -us ` A ) e. NN0_s ) ) )
2 n0sbday 
 |-  ( A e. NN0_s -> ( bday ` A ) e. _om )
3 2 adantl 
 |-  ( ( A e. No /\ A e. NN0_s ) -> ( bday ` A ) e. _om )
4 negsbday 
 |-  ( A e. No -> ( bday ` ( -us ` A ) ) = ( bday ` A ) )
5 4 adantr 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( bday ` ( -us ` A ) ) = ( bday ` A ) )
6 n0sbday 
 |-  ( ( -us ` A ) e. NN0_s -> ( bday ` ( -us ` A ) ) e. _om )
7 6 adantl 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( bday ` ( -us ` A ) ) e. _om )
8 5 7 eqeltrrd 
 |-  ( ( A e. No /\ ( -us ` A ) e. NN0_s ) -> ( bday ` A ) e. _om )
9 3 8 jaodan 
 |-  ( ( A e. No /\ ( A e. NN0_s \/ ( -us ` A ) e. NN0_s ) ) -> ( bday ` A ) e. _om )
10 1 9 sylbi 
 |-  ( A e. ZZ_s -> ( bday ` A ) e. _om )