Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Surreal numbers - cuts and options
oldval
Next ⟩
newval
Metamath Proof Explorer
Ascii
Unicode
Theorem
oldval
Description:
The value of the old options function.
(Contributed by
Scott Fenton
, 6-Aug-2024)
Ref
Expression
Assertion
oldval
⊢
A
∈
On
→
Old
⁡
A
=
⋃
M
A
Proof
Step
Hyp
Ref
Expression
1
df-made
⊢
M
=
recs
⁡
x
∈
V
⟼
|
s
𝒫
⋃
ran
⁡
x
×
𝒫
⋃
ran
⁡
x
2
recsfnon
⊢
recs
⁡
x
∈
V
⟼
|
s
𝒫
⋃
ran
⁡
x
×
𝒫
⋃
ran
⁡
x
Fn
On
3
fnfun
⊢
recs
⁡
x
∈
V
⟼
|
s
𝒫
⋃
ran
⁡
x
×
𝒫
⋃
ran
⁡
x
Fn
On
→
Fun
⁡
recs
⁡
x
∈
V
⟼
|
s
𝒫
⋃
ran
⁡
x
×
𝒫
⋃
ran
⁡
x
4
2
3
ax-mp
⊢
Fun
⁡
recs
⁡
x
∈
V
⟼
|
s
𝒫
⋃
ran
⁡
x
×
𝒫
⋃
ran
⁡
x
5
funeq
⊢
M
=
recs
⁡
x
∈
V
⟼
|
s
𝒫
⋃
ran
⁡
x
×
𝒫
⋃
ran
⁡
x
→
Fun
⁡
M
↔
Fun
⁡
recs
⁡
x
∈
V
⟼
|
s
𝒫
⋃
ran
⁡
x
×
𝒫
⋃
ran
⁡
x
6
4
5
mpbiri
⊢
M
=
recs
⁡
x
∈
V
⟼
|
s
𝒫
⋃
ran
⁡
x
×
𝒫
⋃
ran
⁡
x
→
Fun
⁡
M
7
1
6
ax-mp
⊢
Fun
⁡
M
8
funimaexg
⊢
Fun
⁡
M
∧
A
∈
On
→
M
A
∈
V
9
7
8
mpan
⊢
A
∈
On
→
M
A
∈
V
10
9
uniexd
⊢
A
∈
On
→
⋃
M
A
∈
V
11
imaeq2
⊢
x
=
A
→
M
x
=
M
A
12
11
unieqd
⊢
x
=
A
→
⋃
M
x
=
⋃
M
A
13
df-old
⊢
Old
=
x
∈
On
⟼
⋃
M
x
14
12
13
fvmptg
⊢
A
∈
On
∧
⋃
M
A
∈
V
→
Old
⁡
A
=
⋃
M
A
15
10
14
mpdan
⊢
A
∈
On
→
Old
⁡
A
=
⋃
M
A