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

Proof

Step	Hyp	Ref	Expression
1		sltsolem1	⊢ { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } Or ( { 1o , 2o } ∪ { ∅ } )
2		df-no	⊢ No = { 𝑓 ∣ ∃ 𝑥 ∈ On 𝑓 : 𝑥 ⟶ { 1o , 2o } }
3		df-slt	⊢ <s = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃ 𝑥 ∈ On ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ∧ ( 𝑓 ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝑔 ‘ 𝑥 ) ) ) }
4		nosgnn0	⊢ ¬ ∅ ∈ { 1o , 2o }
5	1 2 3 4	soseq	⊢ <s Or No