Theorem hlclat 40110

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

Syntax hints:   → wi 4   ∈ wcel 2143  CLatccla 18555  OMLcoml 39927  CvLatclc 40017  HLchlt 40102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-hlat 40103

This theorem is referenced by:  hlomcmat  40117  glbconN  40129  pmaple  40513  pmapglbx  40521  polsubN  40659  2polvalN  40666  2polssN  40667  3polN  40668  2pmaplubN  40678  paddunN  40679  poldmj1N  40680  pnonsingN  40685  ispsubcl2N  40699  psubclinN  40700  paddatclN  40701  polsubclN  40704  poml4N  40705  diaglbN  41807  diaintclN  41810  dibglbN  41918  dibintclN  41919  dihglblem2N  42046  dihglblem3N  42047  dihglblem4  42049  dihglbcpreN  42052  dihglblem6  42092  dihintcl  42096  dochval2  42104  dochcl  42105  dochvalr  42109  dochss  42117