| 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 39362 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) | |
| 2 | olop 39215 | . 2 ⊢ (𝐾 ∈ OL → 𝐾 ∈ OP) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 OPcops 39173 OLcol 39175 HLchlt 39351 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-iota 6514 df-fv 6569 df-ov 7434 df-ol 39179 df-oml 39180 df-hlat 39352 |
| This theorem is referenced by: glbconN 39378 glbconNOLD 39379 glbconxN 39380 hlhgt2 39391 hl0lt1N 39392 hl2at 39407 cvrexch 39422 atcvr0eq 39428 lnnat 39429 atle 39438 cvrat4 39445 athgt 39458 1cvrco 39474 1cvratex 39475 1cvrjat 39477 1cvrat 39478 ps-2 39480 llnn0 39518 lplnn0N 39549 llncvrlpln 39560 lvoln0N 39593 lplncvrlvol 39618 dalemkeop 39627 pmapeq0 39768 pmapglb2N 39773 pmapglb2xN 39774 2atm2atN 39787 polval2N 39908 polsubN 39909 pol1N 39912 2polpmapN 39915 2polvalN 39916 poldmj1N 39930 pmapj2N 39931 2polatN 39934 pnonsingN 39935 ispsubcl2N 39949 polsubclN 39954 poml4N 39955 pmapojoinN 39970 pl42lem1N 39981 lhp2lt 40003 lhp0lt 40005 lhpn0 40006 lhpexnle 40008 lhpoc2N 40017 lhpocnle 40018 lhpj1 40024 lhpmod2i2 40040 lhpmod6i1 40041 lhprelat3N 40042 ltrnatb 40139 trlcl 40166 trlle 40186 cdleme3c 40232 cdleme7e 40249 cdleme22b 40343 cdlemg12e 40649 cdlemg12g 40651 tendoid 40775 tendo0tp 40791 cdlemk39s-id 40942 tendoex 40977 dia0eldmN 41042 dia2dimlem2 41067 dia2dimlem3 41068 docaclN 41126 doca2N 41128 djajN 41139 dib0 41166 dih0 41282 dih0bN 41283 dih0rn 41286 dih1 41288 dih1rn 41289 dih1cnv 41290 dihmeetlem18N 41326 dih1dimatlem 41331 dihlspsnssN 41334 dihlspsnat 41335 dihatexv 41340 dihglb2 41344 dochcl 41355 doch0 41360 doch1 41361 dochvalr3 41365 doch2val2 41366 dochss 41367 dochocss 41368 dochoc 41369 dochnoncon 41393 djhlj 41403 dihjatc 41419 |
| Copyright terms: Public domain | W3C validator |