Theorem nomaxmo

Description: A class of surreals has at most one maximum. (Contributed by Scott Fenton, 5-Dec-2021)

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

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		cnvso	$$⊢{<}_s\mathrm{Or}S\leftrightarrow {{<}_s}^{-1}\mathrm{Or}S$$
5	3 4	sylib	$$⊢S\subseteq \mathrm{No}\to {{<}_s}^{-1}\mathrm{Or}S$$
6		somo	$$⊢{{<}_s}^{-1}\mathrm{Or}S\to {\exists }^{*}x\in S\forall y\in S\neg y{{<}_s}^{-1}x$$
7	5 6	syl	$$⊢S\subseteq \mathrm{No}\to {\exists }^{*}x\in S\forall y\in S\neg y{{<}_s}^{-1}x$$
8		vex	$$⊢y\in \mathrm{V}$$
9		vex	$$⊢x\in \mathrm{V}$$
10	8 9	brcnv	$$⊢y{{<}_s}^{-1}x\leftrightarrow x{<}_{s}y$$
11	10	notbii	$$⊢\neg y{{<}_s}^{-1}x\leftrightarrow \neg x{<}_{s}y$$
12	11	ralbii	$$⊢\forall y\in S\neg y{{<}_s}^{-1}x\leftrightarrow \forall y\in S\neg x{<}_{s}y$$
13	12	rmobii	$$⊢{\exists }^{*}x\in S\forall y\in S\neg y{{<}_s}^{-1}x\leftrightarrow {\exists }^{*}x\in S\forall y\in S\neg x{<}_{s}y$$
14	7 13	sylib	$$⊢S\subseteq \mathrm{No}\to {\exists }^{*}x\in S\forall y\in S\neg x{<}_{s}y$$