Theorem nominmo

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

	Ref	Expression
Assertion	nominmo	⊢ ( 𝑆 ⊆ No → ∃* 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ¬ 𝑦 <s 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		sltso	⊢ <s Or No
2		soss	⊢ ( 𝑆 ⊆ No → ( <s Or No → <s Or 𝑆 ) )
3	1 2	mpi	⊢ ( 𝑆 ⊆ No → <s Or 𝑆 )
4		somo	⊢ ( <s Or 𝑆 → ∃* 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ¬ 𝑦 <s 𝑥 )
5	3 4	syl	⊢ ( 𝑆 ⊆ No → ∃* 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ¬ 𝑦 <s 𝑥 )