![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ltso | Structured version Visualization version GIF version |
Description: 'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.) |
Ref | Expression |
---|---|
ltso | ⊢ < Or ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axlttri 11326 | . 2 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 < 𝑦 ↔ ¬ (𝑥 = 𝑦 ∨ 𝑦 < 𝑥))) | |
2 | lttr 11331 | . 2 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 < 𝑦 ∧ 𝑦 < 𝑧) → 𝑥 < 𝑧)) | |
3 | 1, 2 | isso2i 5621 | 1 ⊢ < Or ℝ |
Colors of variables: wff setvar class |
Syntax hints: Or wor 5585 ℝcr 11148 < clt 11289 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5296 ax-nul 5303 ax-pow 5361 ax-pr 5425 ax-un 7738 ax-resscn 11206 ax-pre-lttri 11223 ax-pre-lttrn 11224 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3464 df-sbc 3776 df-csb 3892 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-nul 4323 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4906 df-br 5146 df-opab 5208 df-mpt 5229 df-id 5572 df-po 5586 df-so 5587 df-xp 5680 df-rel 5681 df-cnv 5682 df-co 5683 df-dm 5684 df-rn 5685 df-res 5686 df-ima 5687 df-iota 6498 df-fun 6548 df-fn 6549 df-f 6550 df-f1 6551 df-fo 6552 df-f1o 6553 df-fv 6554 df-er 8726 df-en 8967 df-dom 8968 df-sdom 8969 df-pnf 11291 df-mnf 11292 df-ltxr 11294 |
This theorem is referenced by: gtso 11336 lttri2 11337 lttri3 11338 lttri4 11339 ltnr 11350 ltnsym2 11354 fimaxre 12204 fiminre 12207 lbinf 12213 suprcl 12220 suprub 12221 suprlub 12224 infrecl 12242 infregelb 12244 infrelb 12245 supfirege 12247 suprfinzcl 12722 uzinfi 12958 suprzcl2 12968 suprzub 12969 2resupmax 13215 infmrp1 13371 fseqsupcl 13991 ssnn0fi 13999 fsuppmapnn0fiublem 14004 isercolllem1 15664 isercolllem2 15665 summolem2 15715 zsum 15717 fsumcvg3 15728 mertenslem2 15884 prodmolem2 15932 zprod 15934 cnso 16244 gcdval 16491 dfgcd2 16542 lcmval 16588 lcmgcdlem 16602 odzval 16788 pczpre 16844 prmreclem1 16913 ramz 17022 odval 19528 odf 19531 gexval 19572 gsumval3 19901 retos 21610 mbfsup 25681 mbfinf 25682 itg2monolem1 25768 itg2mono 25771 dvgt0lem2 26024 dvgt0 26025 plyeq0lem 26234 dgrval 26252 dgrcl 26257 dgrub 26258 dgrlb 26260 elqaalem1 26344 elqaalem3 26346 aalioulem2 26358 logccv 26687 ex-po 30365 ssnnssfz 32692 lmdvg 33781 oddpwdc 34201 ballotlemi 34347 ballotlemiex 34348 ballotlemsup 34351 ballotlemimin 34352 ballotlemfrcn0 34376 ballotlemirc 34378 erdszelem3 35034 erdszelem4 35035 erdszelem5 35036 erdszelem6 35037 erdszelem8 35039 erdszelem9 35040 erdszelem11 35042 erdsze2lem1 35044 erdsze2lem2 35045 supfz 35564 inffz 35565 gtinf 36044 ptrecube 37334 poimirlem31 37365 poimirlem32 37366 heicant 37369 mblfinlem3 37373 mblfinlem4 37374 ismblfin 37375 incsequz2 37463 totbndbnd 37503 prdsbnd 37507 aks4d1p4 41791 aks4d1p7 41795 sticksstones1 41858 sticksstones3 41860 sn-suprcld 42184 sn-suprubd 42185 pellfundval 42574 dgraaval 42842 dgraaf 42845 fzisoeu 44951 uzublem 45081 infrglb 45247 limsupubuzlem 45369 fourierdlem25 45789 fourierdlem31 45795 fourierdlem36 45800 fourierdlem37 45801 fourierdlem42 45806 fourierdlem79 45842 ioorrnopnlem 45961 hoicvr 46205 hoidmvlelem2 46253 iunhoiioolem 46332 vonioolem1 46337 fsupdm2 46500 finfdm2 46504 prmdvdsfmtnof1lem1 47192 prmdvdsfmtnof 47194 prmdvdsfmtnof1 47195 ssnn0ssfz 47764 rrx2plordso 48148 |
Copyright terms: Public domain | W3C validator |