Theorem sltso 27759

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 27758	. 2 ⊢ {⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} Or ({1o, 2o} ∪ {∅})
2		df-no 27725	. 2 ⊢ No = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶{1o, 2o}}
3		df-slt 27726	. 2 ⊢ <s = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥)))}
4		nosgnn0 27741	. 2 ⊢ ¬ ∅ ∈ {1o, 2o}
5	1, 2, 3, 4	soseq 8203	1 ⊢ <s Or No

Syntax hints:  ∅c0 4352  {cpr 4650  {ctp 4652  ⟨cop 4654   Or wor 5607  1_oc1o 8518  2_oc2o 8519   No csur 27722   <s cslt 27723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5318  ax-nul 5325  ax-pr 5448

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4933  df-br 5168  df-opab 5230  df-mpt 5251  df-tr 5285  df-id 5594  df-eprel 5600  df-po 5608  df-so 5609  df-fr 5653  df-we 5655  df-xp 5707  df-rel 5708  df-cnv 5709  df-co 5710  df-dm 5711  df-rn 5712  df-res 5713  df-ima 5714  df-ord 6401  df-on 6402  df-suc 6404  df-iota 6528  df-fun 6578  df-fn 6579  df-f 6580  df-fv 6584  df-1o 8525  df-2o 8526  df-no 27725  df-slt 27726

This theorem is referenced by:  nosepne  27763  nosepdm  27767  nodenselem4  27770  nodenselem5  27771  nodenselem7  27773  nolt02o  27778  nogt01o  27779  noresle  27780  nomaxmo  27781  nominmo  27782  nosupprefixmo  27783  noinfprefixmo  27784  nosupbnd1lem1  27791  nosupbnd1lem2  27792  nosupbnd1lem4  27794  nosupbnd1lem6  27796  nosupbnd1  27797  nosupbnd2lem1  27798  nosupbnd2  27799  noinfbnd1lem1  27806  noinfbnd1lem2  27807  noinfbnd1lem4  27809  noinfbnd1lem6  27811  noinfbnd1  27812  noinfbnd2lem1  27813  noinfbnd2  27814  noetasuplem4  27819  noetainflem4  27823  sltirr  27829  slttr  27830  sltasym  27831  sltlin  27832  slttrieq2  27833  slttrine  27834  sleloe  27837  sltletr  27839  slelttr  27840