Theorem sltso 27586

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

Syntax hints:  ∅c0 4284  {cpr 4579  {ctp 4581  ⟨cop 4583   Or wor 5526  1_oc1o 8381  2_oc2o 8382   No csur 27549   <s cslt 27550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-tp 4582  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-ord 6310  df-on 6311  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-fv 6490  df-1o 8388  df-2o 8389  df-no 27552  df-slt 27553

This theorem is referenced by:  nosepne  27590  nosepdm  27594  nodenselem4  27597  nodenselem5  27598  nodenselem7  27600  nolt02o  27605  nogt01o  27606  noresle  27607  nomaxmo  27608  nominmo  27609  nosupprefixmo  27610  noinfprefixmo  27611  nosupbnd1lem1  27618  nosupbnd1lem2  27619  nosupbnd1lem4  27621  nosupbnd1lem6  27623  nosupbnd1  27624  nosupbnd2lem1  27625  nosupbnd2  27626  noinfbnd1lem1  27633  noinfbnd1lem2  27634  noinfbnd1lem4  27636  noinfbnd1lem6  27638  noinfbnd1  27639  noinfbnd2lem1  27640  noinfbnd2  27641  noetasuplem4  27646  noetainflem4  27650  sltirr  27656  slttr  27657  sltasym  27658  sltlin  27659  slttrieq2  27660  slttrine  27661  sleloe  27664  sltletr  27666  slelttr  27667  n0sfincut  28251