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

Theorem hlclat 34173
Description: A Hilbert lattice is complete. (Contributed by NM, 20-Oct-2011.)
Assertion
Ref Expression
hlclat  |-  ( K  e.  HL  ->  K  e.  CLat )

Proof of Theorem hlclat
StepHypRef Expression
1 hlomcmcv 34171 . 2  |-  ( K  e.  HL  ->  ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  CvLat
) )
21simp2d 1009 1  |-  ( K  e.  HL  ->  K  e.  CLat )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   CLatccla 15594   OMLcoml 33990   CvLatclc 34080   HLchlt 34165
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5551  df-fv 5596  df-ov 6287  df-hlat 34166
This theorem is referenced by:  hlomcmat  34179  glbconN  34191  pmaple  34575  pmapglbx  34583  polsubN  34721  2polvalN  34728  2polssN  34729  3polN  34730  2pmaplubN  34740  paddunN  34741  poldmj1N  34742  pnonsingN  34747  ispsubcl2N  34761  psubclinN  34762  paddatclN  34763  polsubclN  34766  poml4N  34767  diaglbN  35870  diaintclN  35873  dibglbN  35981  dibintclN  35982  dihglblem2N  36109  dihglblem3N  36110  dihglblem4  36112  dihglbcpreN  36115  dihglblem6  36155  dihintcl  36159  dochval2  36167  dochcl  36168  dochvalr  36172  dochss  36180
  Copyright terms: Public domain W3C validator