Metamath Proof Explorer

Theorem lrcut

Description: A surreal is equal to the cut of its left and right sets. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Assertion lrcut 
|- ( X e. No -> ( ( _Left ` X ) |s ( _Right ` X ) ) = X )

Proof

Step Hyp Ref Expression
1 bdayelon 
 |-  ( bday ` X ) e. On
2 1 oneli 
 |-  ( b e. ( bday ` X ) -> b e. On )
3 madebday 
 |-  ( ( b e. On /\ y e. No ) -> ( y e. ( _Made ` b ) <-> ( bday ` y ) C_ b ) )
4 3 biimprd 
 |-  ( ( b e. On /\ y e. No ) -> ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) )
5 2 4 sylan 
 |-  ( ( b e. ( bday ` X ) /\ y e. No ) -> ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) )
6 5 rgen2 
 |-  A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) )
7 madebdaylemlrcut 
 |-  ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> ( ( _Left ` X ) |s ( _Right ` X ) ) = X )
8 6 7 mpan 
 |-  ( X e. No -> ( ( _Left ` X ) |s ( _Right ` X ) ) = X )