![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > hlpos | Structured version Visualization version GIF version |
Description: A Hilbert lattice is a poset. (Contributed by NM, 20-Oct-2011.) |
Ref | Expression |
---|---|
hlpos | ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hllat 38139 | . 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) | |
2 | latpos 18378 | . 2 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 Posetcpo 18247 Latclat 18371 HLchlt 38126 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-nul 4321 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4905 df-br 5145 df-opab 5207 df-xp 5678 df-dm 5682 df-iota 6487 df-fv 6543 df-ov 7399 df-lat 18372 df-atl 38074 df-cvlat 38098 df-hlat 38127 |
This theorem is referenced by: hlhgt2 38166 hl0lt1N 38167 cvrval3 38190 cvrexchlem 38196 cvratlem 38198 cvrat 38199 atlelt 38215 2atlt 38216 athgt 38233 1cvratex 38250 ps-2 38255 llnnleat 38290 llncmp 38299 2llnmat 38301 lplnnle2at 38318 llncvrlpln 38335 lplncmp 38339 lvolnle3at 38359 lplncvrlvol 38393 lvolcmp 38394 pmaple 38538 2lnat 38561 2atm2atN 38562 lhp2lt 38778 lhp0lt 38780 dia2dimlem2 39842 dia2dimlem3 39843 dih1 40063 |
Copyright terms: Public domain | W3C validator |