Theorem hlclat 39334

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

Syntax hints:   → wi 4   ∈ wcel 2107  CLatccla 18513  OMLcoml 39151  CvLatclc 39241  HLchlt 39326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-iota 6494  df-fv 6549  df-ov 7416  df-hlat 39327

This theorem is referenced by:  hlomcmat  39341  glbconN  39353  glbconNOLD  39354  pmaple  39738  pmapglbx  39746  polsubN  39884  2polvalN  39891  2polssN  39892  3polN  39893  2pmaplubN  39903  paddunN  39904  poldmj1N  39905  pnonsingN  39910  ispsubcl2N  39924  psubclinN  39925  paddatclN  39926  polsubclN  39929  poml4N  39930  diaglbN  41032  diaintclN  41035  dibglbN  41143  dibintclN  41144  dihglblem2N  41271  dihglblem3N  41272  dihglblem4  41274  dihglbcpreN  41277  dihglblem6  41317  dihintcl  41321  dochval2  41329  dochcl  41330  dochvalr  41334  dochss  41342