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 S No * x S y S ¬ y < s x

Proof

Step Hyp Ref Expression
1 sltso < s Or No
2 soss S No < s Or No < s Or S
3 1 2 mpi S No < s Or S
4 somo < s Or S * x S y S ¬ y < s x
5 3 4 syl S No * x S y S ¬ y < s x