Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Surreal numbers - cuts and options
old0
Next ⟩
madessno
Metamath Proof Explorer
Ascii
Unicode
Theorem
old0
Description:
No surreal is older than
(/)
.
(Contributed by
Scott Fenton
, 7-Aug-2024)
Ref
Expression
Assertion
old0
⊢
Old
⁡
∅
=
∅
Proof
Step
Hyp
Ref
Expression
1
0elon
⊢
∅
∈
On
2
oldval
⊢
∅
∈
On
→
Old
⁡
∅
=
⋃
M
∅
3
1
2
ax-mp
⊢
Old
⁡
∅
=
⋃
M
∅
4
ima0
⊢
M
∅
=
∅
5
4
unieqi
⊢
⋃
M
∅
=
⋃
∅
6
uni0
⊢
⋃
∅
=
∅
7
3
5
6
3eqtri
⊢
Old
⁡
∅
=
∅