Metamath Proof Explorer

Theorem rightgt

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

Ref Expression
Assertion rightgt 
|- ( A e. ( _Right ` B ) -> B

Proof

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