Theorem hlclat 39336

Description: A Hilbert lattice is complete. (Contributed by NM, 20-Oct-2011.)

Assertion

Ref	Expression
hlclat	⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)

Proof of Theorem hlclat

Step	Hyp	Ref	Expression
1		hlomcmcv 39334	. 2 ⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat))
2	1	simp2d 1143	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)

Syntax hints:   → wi 4   ∈ wcel 2109  CLatccla 18422  OMLcoml 39153  CvLatclc 39243  HLchlt 39328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-hlat 39329

This theorem is referenced by:  hlomcmat  39343  glbconN  39355  glbconNOLD  39356  pmaple  39740  pmapglbx  39748  polsubN  39886  2polvalN  39893  2polssN  39894  3polN  39895  2pmaplubN  39905  paddunN  39906  poldmj1N  39907  pnonsingN  39912  ispsubcl2N  39926  psubclinN  39927  paddatclN  39928  polsubclN  39931  poml4N  39932  diaglbN  41034  diaintclN  41037  dibglbN  41145  dibintclN  41146  dihglblem2N  41273  dihglblem3N  41274  dihglblem4  41276  dihglbcpreN  41279  dihglblem6  41319  dihintcl  41323  dochval2  41331  dochcl  41332  dochvalr  41336  dochss  41344