![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > hlclat | Structured version Visualization version GIF version |
Description: A Hilbert lattice is complete. (Contributed by NM, 20-Oct-2011.) |
Ref | Expression |
---|---|
hlclat | ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlomcmcv 38960 | . 2 ⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat)) | |
2 | 1 | simp2d 1140 | 1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 CLatccla 18498 OMLcoml 38779 CvLatclc 38869 HLchlt 38954 |
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-hlat 38955 |
This theorem is referenced by: hlomcmat 38969 glbconN 38981 glbconNOLD 38982 pmaple 39366 pmapglbx 39374 polsubN 39512 2polvalN 39519 2polssN 39520 3polN 39521 2pmaplubN 39531 paddunN 39532 poldmj1N 39533 pnonsingN 39538 ispsubcl2N 39552 psubclinN 39553 paddatclN 39554 polsubclN 39557 poml4N 39558 diaglbN 40660 diaintclN 40663 dibglbN 40771 dibintclN 40772 dihglblem2N 40899 dihglblem3N 40900 dihglblem4 40902 dihglbcpreN 40905 dihglblem6 40945 dihintcl 40949 dochval2 40957 dochcl 40958 dochvalr 40962 dochss 40970 |
Copyright terms: Public domain | W3C validator |