Metamath Proof Explorer

Theorem lruneq

Description: If two surreals share a birthday, then the union of their left and right sets are equal. (Contributed by Scott Fenton, 17-Sep-2024)

Ref Expression
Assertion lruneq 
|- ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( _Left ` X ) u. ( _Right ` X ) ) = ( ( _Left ` Y ) u. ( _Right ` Y ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( ( bday ` X ) = ( bday ` Y ) -> ( _Old ` ( bday ` X ) ) = ( _Old ` ( bday ` Y ) ) )
2 1 3ad2ant3 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( _Old ` ( bday ` X ) ) = ( _Old ` ( bday ` Y ) ) )
3 lrold 
 |-  ( ( _Left ` X ) u. ( _Right ` X ) ) = ( _Old ` ( bday ` X ) )
4 lrold 
 |-  ( ( _Left ` Y ) u. ( _Right ` Y ) ) = ( _Old ` ( bday ` Y ) )
5 2 3 4 3eqtr4g 
 |-  ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) -> ( ( _Left ` X ) u. ( _Right ` X ) ) = ( ( _Left ` Y ) u. ( _Right ` Y ) ) )