Theorem hlclat 39376

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 39374	. 2 ⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat))
2	1	simp2d 1143	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)

Syntax hints:   → wi 4   ∈ wcel 2108  CLatccla 18508  OMLcoml 39193  CvLatclc 39283  HLchlt 39368

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408  df-hlat 39369

This theorem is referenced by:  hlomcmat  39383  glbconN  39395  glbconNOLD  39396  pmaple  39780  pmapglbx  39788  polsubN  39926  2polvalN  39933  2polssN  39934  3polN  39935  2pmaplubN  39945  paddunN  39946  poldmj1N  39947  pnonsingN  39952  ispsubcl2N  39966  psubclinN  39967  paddatclN  39968  polsubclN  39971  poml4N  39972  diaglbN  41074  diaintclN  41077  dibglbN  41185  dibintclN  41186  dihglblem2N  41313  dihglblem3N  41314  dihglblem4  41316  dihglbcpreN  41319  dihglblem6  41359  dihintcl  41363  dochval2  41371  dochcl  41372  dochvalr  41376  dochss  41384