Definition df-no 31040

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

Step	Hyp	Ref	Expression
1		csur 31037	. 2 class No
2		va	. . . . . 6 setvar 𝑎
3	2	cv 1474	. . . . 5 class 𝑎
4		c1o 7440	. . . . . 6 class 1𝑜
5		c2o 7441	. . . . . 6 class 2𝑜
6	4, 5	cpr 4127	. . . . 5 class {1𝑜, 2𝑜}
7		vf	. . . . . 6 setvar 𝑓
8	7	cv 1474	. . . . 5 class 𝑓
9	3, 6, 8	wf 5800	. . . 4 wff 𝑓:𝑎⟶{1𝑜, 2𝑜}
10		con0 5640	. . . 4 class On
11	9, 2, 10	wrex 2897	. . 3 wff ∃𝑎 ∈ On 𝑓:𝑎⟶{1𝑜, 2𝑜}
12	11, 7	cab 2596	. 2 class {𝑓 ∣ ∃𝑎 ∈ On 𝑓:𝑎⟶{1𝑜, 2𝑜}}
13	1, 12	wceq 1475	1 wff No = {𝑓 ∣ ∃𝑎 ∈ On 𝑓:𝑎⟶{1𝑜, 2𝑜}}

This definition is referenced by:  elno  31043  sltso  31068