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 36488
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 36486 . 2 (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat))
21simp2d 1139 1 (𝐾 ∈ HL → 𝐾 ∈ CLat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2110  CLatccla 17711  OMLcoml 36305  CvLatclc 36395  HLchlt 36480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-iota 6309  df-fv 6358  df-ov 7153  df-hlat 36481
This theorem is referenced by:  hlomcmat  36495  glbconN  36507  pmaple  36891  pmapglbx  36899  polsubN  37037  2polvalN  37044  2polssN  37045  3polN  37046  2pmaplubN  37056  paddunN  37057  poldmj1N  37058  pnonsingN  37063  ispsubcl2N  37077  psubclinN  37078  paddatclN  37079  polsubclN  37082  poml4N  37083  diaglbN  38185  diaintclN  38188  dibglbN  38296  dibintclN  38297  dihglblem2N  38424  dihglblem3N  38425  dihglblem4  38427  dihglbcpreN  38430  dihglblem6  38470  dihintcl  38474  dochval2  38482  dochcl  38483  dochvalr  38487  dochss  38495
  Copyright terms: Public domain W3C validator