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 ∈ R ⁡ B → B < s A

Proof

Step Hyp Ref Expression
1 elright ⊢ A ∈ R ⁡ B ↔ A ∈ Old ⁡ bday ⁡ B ∧ B < s A
2 1 simprbi ⊢ A ∈ R ⁡ B → B < s A