Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-no Structured version   Visualization version   GIF version

Definition df-no 30843
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.)

Assertion
Ref Expression
df-no No = {𝑓 ∣ ∃𝑎 ∈ On 𝑓:𝑎⟶{1𝑜, 2𝑜}}
Distinct variable group:   𝑓,𝑎

Detailed syntax breakdown of Definition df-no
StepHypRef Expression
1 csur 30840 . 2 class No
2 va . . . . . 6 setvar 𝑎
32cv 1473 . . . . 5 class 𝑎
4 c1o 7414 . . . . . 6 class 1𝑜
5 c2o 7415 . . . . . 6 class 2𝑜
64, 5cpr 4123 . . . . 5 class {1𝑜, 2𝑜}
7 vf . . . . . 6 setvar 𝑓
87cv 1473 . . . . 5 class 𝑓
93, 6, 8wf 5783 . . . 4 wff 𝑓:𝑎⟶{1𝑜, 2𝑜}
10 con0 5623 . . . 4 class On
119, 2, 10wrex 2893 . . 3 wff 𝑎 ∈ On 𝑓:𝑎⟶{1𝑜, 2𝑜}
1211, 7cab 2592 . 2 class {𝑓 ∣ ∃𝑎 ∈ On 𝑓:𝑎⟶{1𝑜, 2𝑜}}
131, 12wceq 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