![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > hlop | Structured version Visualization version GIF version |
Description: A Hilbert lattice is an orthoposet. (Contributed by NM, 20-Oct-2011.) |
Ref | Expression |
---|---|
hlop | ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlol 38960 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) | |
2 | olop 38813 | . 2 ⊢ (𝐾 ∈ OL → 𝐾 ∈ OP) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 OPcops 38771 OLcol 38773 HLchlt 38949 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-iota 6501 df-fv 6557 df-ov 7422 df-ol 38777 df-oml 38778 df-hlat 38950 |
This theorem is referenced by: glbconN 38976 glbconNOLD 38977 glbconxN 38978 hlhgt2 38989 hl0lt1N 38990 hl2at 39005 cvrexch 39020 atcvr0eq 39026 lnnat 39027 atle 39036 cvrat4 39043 athgt 39056 1cvrco 39072 1cvratex 39073 1cvrjat 39075 1cvrat 39076 ps-2 39078 llnn0 39116 lplnn0N 39147 llncvrlpln 39158 lvoln0N 39191 lplncvrlvol 39216 dalemkeop 39225 pmapeq0 39366 pmapglb2N 39371 pmapglb2xN 39372 2atm2atN 39385 polval2N 39506 polsubN 39507 pol1N 39510 2polpmapN 39513 2polvalN 39514 poldmj1N 39528 pmapj2N 39529 2polatN 39532 pnonsingN 39533 ispsubcl2N 39547 polsubclN 39552 poml4N 39553 pmapojoinN 39568 pl42lem1N 39579 lhp2lt 39601 lhp0lt 39603 lhpn0 39604 lhpexnle 39606 lhpoc2N 39615 lhpocnle 39616 lhpj1 39622 lhpmod2i2 39638 lhpmod6i1 39639 lhprelat3N 39640 ltrnatb 39737 trlcl 39764 trlle 39784 cdleme3c 39830 cdleme7e 39847 cdleme22b 39941 cdlemg12e 40247 cdlemg12g 40249 tendoid 40373 tendo0tp 40389 cdlemk39s-id 40540 tendoex 40575 dia0eldmN 40640 dia2dimlem2 40665 dia2dimlem3 40666 docaclN 40724 doca2N 40726 djajN 40737 dib0 40764 dih0 40880 dih0bN 40881 dih0rn 40884 dih1 40886 dih1rn 40887 dih1cnv 40888 dihmeetlem18N 40924 dih1dimatlem 40929 dihlspsnssN 40932 dihlspsnat 40933 dihatexv 40938 dihglb2 40942 dochcl 40953 doch0 40958 doch1 40959 dochvalr3 40963 doch2val2 40964 dochss 40965 dochocss 40966 dochoc 40967 dochnoncon 40991 djhlj 41001 dihjatc 41017 |
Copyright terms: Public domain | W3C validator |