Metamath Proof Explorer


Theorem nominmo

Description: A class of surreals has at most one minimum. (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Assertion nominmo SNo*xSyS¬y<sx

Proof

Step Hyp Ref Expression
1 sltso <sOrNo
2 soss SNo<sOrNo<sOrS
3 1 2 mpi SNo<sOrS
4 somo <sOrS*xSyS¬y<sx
5 3 4 syl SNo*xSyS¬y<sx