![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sltso | Structured version Visualization version GIF version |
Description: Less-than totally orders the surreals. Axiom O of [Alling] p. 184. (Contributed by Scott Fenton, 9-Jun-2011.) |
Ref | Expression |
---|---|
sltso | ⊢ <s Or No |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sltsolem1 26975 | . 2 ⊢ {⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} Or ({1o, 2o} ∪ {∅}) | |
2 | df-no 26943 | . 2 ⊢ No = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶{1o, 2o}} | |
3 | df-slt 26944 | . 2 ⊢ <s = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥)))} | |
4 | nosgnn0 26958 | . 2 ⊢ ¬ ∅ ∈ {1o, 2o} | |
5 | 1, 2, 3, 4 | soseq 8083 | 1 ⊢ <s Or No |
Colors of variables: wff setvar class |
Syntax hints: ∅c0 4280 {cpr 4586 {ctp 4588 ⟨cop 4590 Or wor 5542 1oc1o 8397 2oc2o 8398 No csur 26940 <s cslt 26941 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-sep 5254 ax-nul 5261 ax-pr 5382 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-sbc 3738 df-csb 3854 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3927 df-nul 4281 df-if 4485 df-pw 4560 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4864 df-br 5104 df-opab 5166 df-mpt 5187 df-tr 5221 df-id 5529 df-eprel 5535 df-po 5543 df-so 5544 df-fr 5586 df-we 5588 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-ord 6318 df-on 6319 df-suc 6321 df-iota 6445 df-fun 6495 df-fn 6496 df-f 6497 df-fv 6501 df-1o 8404 df-2o 8405 df-no 26943 df-slt 26944 |
This theorem is referenced by: nosepne 26980 nosepdm 26984 nodenselem4 26987 nodenselem5 26988 nodenselem7 26990 nolt02o 26995 nogt01o 26996 noresle 26997 nomaxmo 26998 nominmo 26999 nosupprefixmo 27000 noinfprefixmo 27001 nosupbnd1lem1 27008 nosupbnd1lem2 27009 nosupbnd1lem4 27011 nosupbnd1lem6 27013 nosupbnd1 27014 nosupbnd2lem1 27015 nosupbnd2 27016 noinfbnd1lem1 27023 noinfbnd1lem2 27024 noinfbnd1lem4 27026 noinfbnd1lem6 27028 noinfbnd1 27029 noinfbnd2lem1 27030 noinfbnd2 27031 noetasuplem4 27036 noetainflem4 27040 sltirr 27046 slttr 27047 sltasym 27048 sltlin 27049 slttrieq2 27050 slttrine 27051 sleloe 27054 sltletr 27056 slelttr 27057 |
Copyright terms: Public domain | W3C validator |