Theorem hlclat 38276

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

Syntax hints:   → wi 4   ∈ wcel 2107  CLatccla 18451  OMLcoml 38093  CvLatclc 38183  HLchlt 38268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-hlat 38269

This theorem is referenced by:  hlomcmat  38283  glbconN  38295  glbconNOLD  38296  pmaple  38680  pmapglbx  38688  polsubN  38826  2polvalN  38833  2polssN  38834  3polN  38835  2pmaplubN  38845  paddunN  38846  poldmj1N  38847  pnonsingN  38852  ispsubcl2N  38866  psubclinN  38867  paddatclN  38868  polsubclN  38871  poml4N  38872  diaglbN  39974  diaintclN  39977  dibglbN  40085  dibintclN  40086  dihglblem2N  40213  dihglblem3N  40214  dihglblem4  40216  dihglbcpreN  40219  dihglblem6  40259  dihintcl  40263  dochval2  40271  dochcl  40272  dochvalr  40276  dochss  40284