Theorem nominmo

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

	Ref	Expression
Assertion	nominmo	$$⊢S\subseteq \mathrm{No}\to {\exists }^{*}x\in S\forall y\in S\neg y{<}_{s}x$$

Proof

Step	Hyp	Ref	Expression
1		ltsso	$$⊢{<}_s\mathrm{Or}\mathrm{No}$$
2		soss	$$⊢S\subseteq \mathrm{No}\to \left({<}_s\mathrm{Or}\mathrm{No}\to {<}_s\mathrm{Or}S\right)$$
3	1 2	mpi	$$⊢S\subseteq \mathrm{No}\to {<}_s\mathrm{Or}S$$
4		somo	$$⊢{<}_s\mathrm{Or}S\to {\exists }^{*}x\in S\forall y\in S\neg y{<}_{s}x$$
5	3 4	syl	$$⊢S\subseteq \mathrm{No}\to {\exists }^{*}x\in S\forall y\in S\neg y{<}_{s}x$$