Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Surreal numbers - cuts and options
newval
Next ⟩
madef
Metamath Proof Explorer
Ascii
Unicode
Theorem
newval
Description:
The value of the new options function.
(Contributed by
Scott Fenton
, 6-Aug-2024)
Ref
Expression
Assertion
newval
⊢
A
∈
On
→
N
⁡
A
=
M
⁡
A
∖
Old
⁡
A
Proof
Step
Hyp
Ref
Expression
1
fveq2
⊢
x
=
A
→
M
⁡
x
=
M
⁡
A
2
fveq2
⊢
x
=
A
→
Old
⁡
x
=
Old
⁡
A
3
1
2
difeq12d
⊢
x
=
A
→
M
⁡
x
∖
Old
⁡
x
=
M
⁡
A
∖
Old
⁡
A
4
df-new
⊢
N
=
x
∈
On
⟼
M
⁡
x
∖
Old
⁡
x
5
fvex
⊢
M
⁡
A
∈
V
6
5
difexi
⊢
M
⁡
A
∖
Old
⁡
A
∈
V
7
3
4
6
fvmpt
⊢
A
∈
On
→
N
⁡
A
=
M
⁡
A
∖
Old
⁡
A