Theorem hlclat 40173

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  CLatccla 18579  OMLcoml 39990  CvLatclc 40080  HLchlt 40165

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426  df-hlat 40166

This theorem is used by:  hlomcmat  40180  glbconN  40192  pmaple  40576  pmapglbx  40584  polsubN  40722  2polvalN  40729  2polssN  40730  3polN  40731  2pmaplubN  40741  paddunN  40742  poldmj1N  40743  pnonsingN  40748  ispsubcl2N  40762  psubclinN  40763  paddatclN  40764  polsubclN  40767  poml4N  40768  diaglbN  41870  diaintclN  41873  dibglbN  41981  dibintclN  41982  dihglblem2N  42109  dihglblem3N  42110  dihglblem4  42112  dihglbcpreN  42115  dihglblem6  42155  dihintcl  42159  dochval2  42167  dochcl  42168  dochvalr  42172  dochss  42180