Theorem sltso 26904

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

Assertion

Ref	Expression
sltso	⊢ <s Or No

Proof of Theorem sltso

Dummy variables 𝑓 𝑔 𝑥 𝑦 are mutually distinct and distinct from all other variables.

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

Syntax hints:  ∅c0 4266  {cpr 4572  {ctp 4574  ⟨cop 4576   Or wor 5519  1_oc1o 8338  2_oc2o 8339   No csur 26868   <s cslt 26869

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pr 5366

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3442  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-pss 3915  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-uni 4850  df-br 5087  df-opab 5149  df-mpt 5170  df-tr 5204  df-id 5506  df-eprel 5512  df-po 5520  df-so 5521  df-fr 5562  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-ord 6291  df-on 6292  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-fv 6473  df-1o 8345  df-2o 8346  df-no 26871  df-slt 26872

This theorem is referenced by:  nosepne  26908  nosepdm  26912  nodenselem4  26915  nodenselem5  26916  nodenselem7  26918  nolt02o  33968  nogt01o  33969  noresle  33970  nomaxmo  33971  nominmo  33972  nosupprefixmo  33973  noinfprefixmo  33974  nosupbnd1lem1  33981  nosupbnd1lem2  33982  nosupbnd1lem4  33984  nosupbnd1lem6  33986  nosupbnd1  33987  nosupbnd2lem1  33988  nosupbnd2  33989  noinfbnd1lem1  33996  noinfbnd1lem2  33997  noinfbnd1lem4  33999  noinfbnd1lem6  34001  noinfbnd1  34002  noinfbnd2lem1  34003  noinfbnd2  34004  noetasuplem4  34009  noetainflem4  34013  sltirr  34019  slttr  34020  sltasym  34021  sltlin  34022  slttrieq2  34023  slttrine  34024  sleloe  34027  sltletr  34029  slelttr  34030