Definition df-no

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 Gonshor, and is based on the conception of a "sign expansion" of a surreal number. We define the surreals as ordinal-indexed sequences of 1o and 2o , analagous to Gonshor'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
Assertion	df-no	$$⊢\mathrm{No}=\left\{f|\exists a\in \mathrm{On}f:a⟶\left\{1_{𝑜},2_{𝑜}\right\}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csur	$$class\mathrm{No}$$
1		vf	$$setvarf$$
2		va	$$setvara$$
3		con0	$$class\mathrm{On}$$
4	1	cv	$$setvarf$$
5	2	cv	$$setvara$$
6		c1o	$$class{1}_{𝑜}$$
7		c2o	$$class{2}_{𝑜}$$
8	6 7	cpr	$$class\left\{1_{𝑜},2_{𝑜}\right\}$$
9	5 8 4	wf	$$wfff:a⟶\left\{1_{𝑜},2_{𝑜}\right\}$$
10	9 2 3	wrex	$$wff\exists a\in \mathrm{On}f:a⟶\left\{1_{𝑜},2_{𝑜}\right\}$$
11	10 1	cab	$$class\left\{f|\exists a\in \mathrm{On}f:a⟶\left\{1_{𝑜},2_{𝑜}\right\}\right\}$$
12	0 11	wceq	$$wff\mathrm{No}=\left\{f|\exists a\in \mathrm{On}f:a⟶\left\{1_{𝑜},2_{𝑜}\right\}\right\}$$