Metamath Proof Explorer

Theorem leftirr

Description: No surreal is a member of its left set. (Contributed by Scott Fenton, 9-Oct-2024)

Ref Expression
Assertion leftirr 
|- -. X e. ( _L ` X )

Proof

Step Hyp Ref Expression
1 oldirr 
 |-  -. X e. ( _Old ` ( bday ` X ) )
2 leftssold 
 |-  ( _L ` X ) C_ ( _Old ` ( bday ` X ) )
3 2 sseli 
 |-  ( X e. ( _L ` X ) -> X e. ( _Old ` ( bday ` X ) ) )
4 1 3 mto 
 |-  -. X e. ( _L ` X )