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 33666 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) | |
2 | olop 33519 | . 2 ⊢ (𝐾 ∈ OL → 𝐾 ∈ OP) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1977 OPcops 33477 OLcol 33479 HLchlt 33655 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-iota 5768 df-fv 5812 df-ov 6552 df-ol 33483 df-oml 33484 df-hlat 33656 |
This theorem is referenced by: glbconN 33681 glbconxN 33682 hlhgt2 33693 hl0lt1N 33694 hl2at 33709 cvrexch 33724 atcvr0eq 33730 lnnat 33731 atle 33740 cvrat4 33747 athgt 33760 1cvrco 33776 1cvratex 33777 1cvrjat 33779 1cvrat 33780 ps-2 33782 llnn0 33820 lplnn0N 33851 llncvrlpln 33862 lvoln0N 33895 lplncvrlvol 33920 dalemkeop 33929 pmapeq0 34070 pmapglb2N 34075 pmapglb2xN 34076 2atm2atN 34089 polval2N 34210 polsubN 34211 pol1N 34214 2polpmapN 34217 2polvalN 34218 poldmj1N 34232 pmapj2N 34233 2polatN 34236 pnonsingN 34237 ispsubcl2N 34251 polsubclN 34256 poml4N 34257 pmapojoinN 34272 pl42lem1N 34283 lhp2lt 34305 lhp0lt 34307 lhpn0 34308 lhpexnle 34310 lhpoc2N 34319 lhpocnle 34320 lhpj1 34326 lhpmod2i2 34342 lhpmod6i1 34343 lhprelat3N 34344 ltrnatb 34441 ltrnmwOLD 34456 trlcl 34469 trlle 34489 cdleme3c 34535 cdleme7e 34552 cdleme22b 34647 cdlemg12e 34953 cdlemg12g 34955 tendoid 35079 tendo0tp 35095 cdlemk39s-id 35246 tendoex 35281 dia0eldmN 35347 dia2dimlem2 35372 dia2dimlem3 35373 docaclN 35431 doca2N 35433 djajN 35444 dib0 35471 dih0 35587 dih0bN 35588 dih0rn 35591 dih1 35593 dih1rn 35594 dih1cnv 35595 dihmeetlem18N 35631 dih1dimatlem 35636 dihlspsnssN 35639 dihlspsnat 35640 dihatexv 35645 dihglb2 35649 dochcl 35660 doch0 35665 doch1 35666 dochvalr3 35670 doch2val2 35671 dochss 35672 dochocss 35673 dochoc 35674 dochnoncon 35698 djhlj 35708 dihjatc 35724 |
Copyright terms: Public domain | W3C validator |