Theorem ltsso 28063

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

Assertion

Ref	Expression
ltsso	⊢ <s Or No

Proof of Theorem ltsso

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

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

This proof depends on syntax axioms:  ∅c0 4281  {cpr 4590  {ctp 4592  ⟨cop 4838   Or wor 5562  1_oc1o 8497  2_oc2o 8498  Nocsur 28027   <s clts 28028

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-ord 6383  df-on 6384  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-fv 6566  df-1o 8504  df-2o 8505  df-no 28030  df-lts 28031

This theorem is used by:  nosepne  28067  nosepdm  28071  nodenselem4  28074  nodenselem5  28075  nodenselem7  28077  nolt02o  28082  nogt01o  28083  noresle  28084  nomaxmo  28085  nominmo  28086  nosupprefixmo  28087  noinfprefixmo  28088  nosupbnd1lem1  28095  nosupbnd1lem2  28096  nosupbnd1lem4  28098  nosupbnd1lem6  28100  nosupbnd1  28101  nosupbnd2lem1  28102  nosupbnd2  28103  noinfbnd1lem1  28110  noinfbnd1lem2  28111  noinfbnd1lem4  28113  noinfbnd1lem6  28115  noinfbnd1  28116  noinfbnd2lem1  28117  noinfbnd2  28118  noetasuplem4  28123  noetainflem4  28127  ltsirr  28133  ltstr  28134  ltsasym  28135  ltslin  28136  ltstrieq2  28137  ltstrine  28138  lesloe  28141  ltlestr  28147  leltstr  28148  n0fincut  28771  bdayfinbndlem1  28883