Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Surreal Numbers: Full-Eta Property
nominmo
Next ⟩
nosupprefixmo
Metamath Proof Explorer
Ascii
Unicode
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