Mathbox for Scott Fenton |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-no | Structured version Visualization version GIF version |
Description: Define the class of
surreal numbers. The surreal numbers are a proper
class of numbers developed by John H. Conway and introduced by Donald
Knuth in 1975. They form a proper class into which all ordered fields
can be embedded. The approach we take to defining them was first
introduced by Hary Goshnor, and is based on the conception of a
"sign
expansion" of a surreal number. We define the surreals as
ordinal-indexed sequences of 1_{𝑜} and 2_{𝑜}, analagous to Goshnor's
( − ) and ( + ).
After introducing this definition, we will abstract away from it using axioms that Norman Alling developed in "Foundations of Analysis over Surreal Number Fields." This is done in an effort to be agnostic towards the exact implementation of surreals. (Contributed by Scott Fenton, 9-Jun-2011.) |
Ref | Expression |
---|---|
df-no | ⊢ No = {𝑓 ∣ ∃𝑎 ∈ On 𝑓:𝑎⟶{1_{𝑜}, 2_{𝑜}}} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csur 30840 | . 2 class No | |
2 | va | . . . . . 6 setvar 𝑎 | |
3 | 2 | cv 1473 | . . . . 5 class 𝑎 |
4 | c1o 7414 | . . . . . 6 class 1_{𝑜} | |
5 | c2o 7415 | . . . . . 6 class 2_{𝑜} | |
6 | 4, 5 | cpr 4123 | . . . . 5 class {1_{𝑜}, 2_{𝑜}} |
7 | vf | . . . . . 6 setvar 𝑓 | |
8 | 7 | cv 1473 | . . . . 5 class 𝑓 |
9 | 3, 6, 8 | wf 5783 | . . . 4 wff 𝑓:𝑎⟶{1_{𝑜}, 2_{𝑜}} |
10 | con0 5623 | . . . 4 class On | |
11 | 9, 2, 10 | wrex 2893 | . . 3 wff ∃𝑎 ∈ On 𝑓:𝑎⟶{1_{𝑜}, 2_{𝑜}} |
12 | 11, 7 | cab 2592 | . 2 class {𝑓 ∣ ∃𝑎 ∈ On 𝑓:𝑎⟶{1_{𝑜}, 2_{𝑜}}} |
13 | 1, 12 | wceq 1474 | 1 wff No = {𝑓 ∣ ∃𝑎 ∈ On 𝑓:𝑎⟶{1_{𝑜}, 2_{𝑜}}} |
Colors of variables: wff setvar class |
This definition is referenced by: elno 30846 sltso 30871 |
Copyright terms: Public domain | W3C validator |