Theorem hlclat 37299

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

Syntax hints:   → wi 4   ∈ wcel 2108  CLatccla 18131  OMLcoml 37116  CvLatclc 37206  HLchlt 37291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-hlat 37292

This theorem is referenced by:  hlomcmat  37306  glbconN  37318  pmaple  37702  pmapglbx  37710  polsubN  37848  2polvalN  37855  2polssN  37856  3polN  37857  2pmaplubN  37867  paddunN  37868  poldmj1N  37869  pnonsingN  37874  ispsubcl2N  37888  psubclinN  37889  paddatclN  37890  polsubclN  37893  poml4N  37894  diaglbN  38996  diaintclN  38999  dibglbN  39107  dibintclN  39108  dihglblem2N  39235  dihglblem3N  39236  dihglblem4  39238  dihglbcpreN  39241  dihglblem6  39281  dihintcl  39285  dochval2  39293  dochcl  39294  dochvalr  39298  dochss  39306