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	|-

Proof

Step	Hyp	Ref	Expression
1		sltsolem1	|- { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } Or ( { 1o , 2o } u. { (/) } )
2		df-no	|- No = { f | E. x e. On f : x --> { 1o , 2o } }
3		df-slt	|- . | ( ( f e. No /\ g e. No ) /\ E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) ) ) }
4		nosgnn0	|- -. (/) e. { 1o , 2o }
5	1 2 3 4	soseq	|-