Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > xrltso | Structured version Visualization version GIF version |
Description: 'Less than' is a strict ordering on the extended reals. (Contributed by NM, 15-Oct-2005.) |
Ref | Expression |
---|---|
xrltso | ⊢ < Or ℝ* |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xrlttri 12617 | . 2 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑥 < 𝑦 ↔ ¬ (𝑥 = 𝑦 ∨ 𝑦 < 𝑥))) | |
2 | xrlttr 12618 | . 2 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*) → ((𝑥 < 𝑦 ∧ 𝑦 < 𝑧) → 𝑥 < 𝑧)) | |
3 | 1, 2 | isso2i 5477 | 1 ⊢ < Or ℝ* |
Colors of variables: wff setvar class |
Syntax hints: Or wor 5441 ℝ*cxr 10754 < clt 10755 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710 ax-sep 5167 ax-nul 5174 ax-pow 5232 ax-pr 5296 ax-un 7481 ax-cnex 10673 ax-resscn 10674 ax-pre-lttri 10691 ax-pre-lttrn 10692 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3400 df-sbc 3681 df-csb 3791 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-nul 4212 df-if 4415 df-pw 4490 df-sn 4517 df-pr 4519 df-op 4523 df-uni 4797 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5429 df-po 5442 df-so 5443 df-xp 5531 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-rn 5536 df-res 5537 df-ima 5538 df-iota 6297 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 df-fv 6347 df-er 8322 df-en 8558 df-dom 8559 df-sdom 8560 df-pnf 10757 df-mnf 10758 df-xr 10759 df-ltxr 10760 |
This theorem is referenced by: xrlttri2 12620 xrlttri3 12621 xrltne 12641 xmullem 12742 xmulasslem 12763 supxr 12791 supxrcl 12793 supxrun 12794 supxrmnf 12795 supxrunb1 12797 supxrunb2 12798 supxrub 12802 supxrlub 12803 infxrcl 12811 infxrlb 12812 infxrgelb 12813 xrinf0 12816 infmremnf 12821 limsupval 14923 limsupgval 14925 limsupgre 14930 ramval 16446 ramcl2lem 16447 prdsdsfn 16843 prdsdsval 16856 imasdsfn 16892 imasdsval 16893 prdsmet 23125 xpsdsval 23136 prdsbl 23246 tmsxpsval2 23294 nmoval 23470 xrge0tsms2 23589 metdsval 23601 iccpnfhmeo 23699 xrhmeo 23700 ovolval 24227 ovolf 24236 ovolctb 24244 itg2val 24483 mdegval 24818 mdegldg 24821 mdegxrf 24823 mdegcl 24824 aannenlem2 25079 nmooval 28700 nmoo0 28728 nmopval 29793 nmfnval 29813 nmop0 29923 nmfn0 29924 xrsupssd 30659 xrge0infssd 30661 infxrge0lb 30664 infxrge0glb 30665 infxrge0gelb 30666 xrsclat 30868 xrge0iifiso 31459 esumval 31586 esumnul 31588 esum0 31589 gsumesum 31599 esumsnf 31604 esumpcvgval 31618 esum2d 31633 omsfval 31833 omsf 31835 oms0 31836 omssubaddlem 31838 omssubadd 31839 mblfinlem2 35460 ovoliunnfl 35464 voliunnfl 35466 volsupnfl 35467 itg2addnclem 35473 radcnvrat 41492 infxrglb 42439 xrgtso 42444 infxr 42466 infxrunb2 42467 infxrpnf 42547 limsup0 42799 limsuppnfdlem 42806 limsupequzlem 42827 supcnvlimsup 42845 limsuplt2 42858 liminfval 42864 limsupge 42866 liminfgval 42867 liminfval2 42873 limsup10ex 42878 liminf10ex 42879 liminflelimsuplem 42880 cnrefiisplem 42934 etransclem48 43387 sge0val 43468 sge0z 43477 sge00 43478 sge0sn 43481 sge0tsms 43482 ovnval2 43647 smflimsuplem1 43914 smflimsuplem2 43915 smflimsuplem4 43917 smflimsuplem7 43920 |
Copyright terms: Public domain | W3C validator |