Metamath Proof Explorer

Theorem leftlt

Description: A member of a surreal's left set is less than it. (Contributed by Scott Fenton, 7-Nov-2025)

Ref Expression
Assertion leftlt 
|- ( A e. ( _Left ` B ) -> A

Proof

Step Hyp Ref Expression
1 elleft 
 |-  ( A e. ( _Left ` B ) <-> ( A e. ( _Old ` ( bday ` B ) ) /\ A
2 1 simprbi 
 |-  ( A e. ( _Left ` B ) -> A