Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hlclat Structured version   Visualization version   GIF version

Theorem hlclat 38962
Description: A Hilbert lattice is complete. (Contributed by NM, 20-Oct-2011.)
Assertion
Ref Expression
hlclat (𝐾 ∈ HL → 𝐾 ∈ CLat)

Proof of Theorem hlclat
StepHypRef Expression
1 hlomcmcv 38960 . 2 (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat))
21simp2d 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