Theorem nominmo

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

	Ref	Expression
Assertion	nominmo	|- ( S C_ No -> E* x e. S A. y e. S -. y

Proof

Step	Hyp	Ref	Expression
1		sltso	|-
2		soss	|- ( S C_ No -> (
3	1 2	mpi	|- ( S C_ No ->
4		somo	|- ( E* x e. S A. y e. S -. y
5	3 4	syl	|- ( S C_ No -> E* x e. S A. y e. S -. y