Theorem sltso

Description: Surreal less than totally orders the surreals. Axiom O of Alling p. 184. (Contributed by Scott Fenton, 9-Jun-2011)

	Ref	Expression
Assertion	sltso	$$⊢{<}_s\mathrm{Or}\mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		sltsolem1	$$⊢\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}\mathrm{Or}\left(\left\{1_{𝑜},2_{𝑜}\right\}\cup \left\{\varnothing \right\}\right)$$
2		df-no	$$⊢\mathrm{No}=\left\{f|\exists x\in \mathrm{On}f:x⟶\left\{1_{𝑜},2_{𝑜}\right\}\right\}$$
3		df-slt	$$⊢{<}_s=\left\{⟨f,g⟩|\left(\left(f\in \mathrm{No}\wedge g\in \mathrm{No}\right)\wedge \exists x\in \mathrm{On}\left(\forall y\in xf\left(y\right)=g\left(y\right)\wedge f\left(x\right)\left\{⟨1_{𝑜},\varnothing ⟩,⟨1_{𝑜},2_{𝑜}⟩,⟨\varnothing ,2_{𝑜}⟩\right\}g\left(x\right)\right)\right)\right\}$$
4		nosgnn0	$$⊢\neg \varnothing \in \left\{1_{𝑜},2_{𝑜}\right\}$$
5	1 2 3 4	soseq	$$⊢{<}_s\mathrm{Or}\mathrm{No}$$