![]() |
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 35948 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) | |
2 | olop 35801 | . 2 ⊢ (𝐾 ∈ OL → 𝐾 ∈ OP) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2050 OPcops 35759 OLcol 35761 HLchlt 35937 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-nul 4179 df-if 4351 df-sn 4442 df-pr 4444 df-op 4448 df-uni 4713 df-br 4930 df-iota 6152 df-fv 6196 df-ov 6979 df-ol 35765 df-oml 35766 df-hlat 35938 |
This theorem is referenced by: glbconN 35964 glbconxN 35965 hlhgt2 35976 hl0lt1N 35977 hl2at 35992 cvrexch 36007 atcvr0eq 36013 lnnat 36014 atle 36023 cvrat4 36030 athgt 36043 1cvrco 36059 1cvratex 36060 1cvrjat 36062 1cvrat 36063 ps-2 36065 llnn0 36103 lplnn0N 36134 llncvrlpln 36145 lvoln0N 36178 lplncvrlvol 36203 dalemkeop 36212 pmapeq0 36353 pmapglb2N 36358 pmapglb2xN 36359 2atm2atN 36372 polval2N 36493 polsubN 36494 pol1N 36497 2polpmapN 36500 2polvalN 36501 poldmj1N 36515 pmapj2N 36516 2polatN 36519 pnonsingN 36520 ispsubcl2N 36534 polsubclN 36539 poml4N 36540 pmapojoinN 36555 pl42lem1N 36566 lhp2lt 36588 lhp0lt 36590 lhpn0 36591 lhpexnle 36593 lhpoc2N 36602 lhpocnle 36603 lhpj1 36609 lhpmod2i2 36625 lhpmod6i1 36626 lhprelat3N 36627 ltrnatb 36724 trlcl 36751 trlle 36771 cdleme3c 36817 cdleme7e 36834 cdleme22b 36928 cdlemg12e 37234 cdlemg12g 37236 tendoid 37360 tendo0tp 37376 cdlemk39s-id 37527 tendoex 37562 dia0eldmN 37627 dia2dimlem2 37652 dia2dimlem3 37653 docaclN 37711 doca2N 37713 djajN 37724 dib0 37751 dih0 37867 dih0bN 37868 dih0rn 37871 dih1 37873 dih1rn 37874 dih1cnv 37875 dihmeetlem18N 37911 dih1dimatlem 37916 dihlspsnssN 37919 dihlspsnat 37920 dihatexv 37925 dihglb2 37929 dochcl 37940 doch0 37945 doch1 37946 dochvalr3 37950 doch2val2 37951 dochss 37952 dochocss 37953 dochoc 37954 dochnoncon 37978 djhlj 37988 dihjatc 38004 |
Copyright terms: Public domain | W3C validator |