Theorem hlclat 40508

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  CLatccla 18677  OMLcoml 40325  CvLatclc 40415  HLchlt 40500

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-hlat 40501

This theorem is used by:  hlomcmat  40515  glbconN  40527  pmaple  40911  pmapglbx  40919  polsubN  41057  2polvalN  41064  2polssN  41065  3polN  41066  2pmaplubN  41076  paddunN  41077  poldmj1N  41078  pnonsingN  41083  ispsubcl2N  41097  psubclinN  41098  paddatclN  41099  polsubclN  41102  poml4N  41103  diaglbN  42205  diaintclN  42208  dibglbN  42316  dibintclN  42317  dihglblem2N  42444  dihglblem3N  42445  dihglblem4  42447  dihglbcpreN  42450  dihglblem6  42490  dihintcl  42494  dochval2  42502  dochcl  42503  dochvalr  42507  dochss  42515