Metamath Proof Explorer

Theorem bday11on

Description: The birthday function is one-to-one over the surreal ordinals. (Contributed by Scott Fenton, 6-Nov-2025)

Ref Expression
Assertion bday11on 
|- ( ( A e. On_s /\ B e. On_s /\ ( bday ` A ) = ( bday ` B ) ) -> A = B )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( ( bday ` A ) = ( bday ` B ) -> ( _Old ` ( bday ` A ) ) = ( _Old ` ( bday ` B ) ) )
2 1 3ad2ant3 
 |-  ( ( A e. On_s /\ B e. On_s /\ ( bday ` A ) = ( bday ` B ) ) -> ( _Old ` ( bday ` A ) ) = ( _Old ` ( bday ` B ) ) )
3 onsleft 
 |-  ( A e. On_s -> ( _Old ` ( bday ` A ) ) = ( _Left ` A ) )
4 3 3ad2ant1 
 |-  ( ( A e. On_s /\ B e. On_s /\ ( bday ` A ) = ( bday ` B ) ) -> ( _Old ` ( bday ` A ) ) = ( _Left ` A ) )
5 onsleft 
 |-  ( B e. On_s -> ( _Old ` ( bday ` B ) ) = ( _Left ` B ) )
6 5 3ad2ant2 
 |-  ( ( A e. On_s /\ B e. On_s /\ ( bday ` A ) = ( bday ` B ) ) -> ( _Old ` ( bday ` B ) ) = ( _Left ` B ) )
7 2 4 6 3eqtr3d 
 |-  ( ( A e. On_s /\ B e. On_s /\ ( bday ` A ) = ( bday ` B ) ) -> ( _Left ` A ) = ( _Left ` B ) )
8 7 oveq1d 
 |-  ( ( A e. On_s /\ B e. On_s /\ ( bday ` A ) = ( bday ` B ) ) -> ( ( _Left ` A ) |s (/) ) = ( ( _Left ` B ) |s (/) ) )
9 onscutleft 
 |-  ( A e. On_s -> A = ( ( _Left ` A ) |s (/) ) )
10 9 3ad2ant1 
 |-  ( ( A e. On_s /\ B e. On_s /\ ( bday ` A ) = ( bday ` B ) ) -> A = ( ( _Left ` A ) |s (/) ) )
11 onscutleft 
 |-  ( B e. On_s -> B = ( ( _Left ` B ) |s (/) ) )
12 11 3ad2ant2 
 |-  ( ( A e. On_s /\ B e. On_s /\ ( bday ` A ) = ( bday ` B ) ) -> B = ( ( _Left ` B ) |s (/) ) )
13 8 10 12 3eqtr4d 
 |-  ( ( A e. On_s /\ B e. On_s /\ ( bday ` A ) = ( bday ` B ) ) -> A = B )