Theorem hlclat 38962

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

Syntax hints:   → wi 4   ∈ wcel 2098  CLatccla 18498  OMLcoml 38779  CvLatclc 38869  HLchlt 38954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-iota 6501  df-fv 6557  df-ov 7422  df-hlat 38955

This theorem is referenced by:  hlomcmat  38969  glbconN  38981  glbconNOLD  38982  pmaple  39366  pmapglbx  39374  polsubN  39512  2polvalN  39519  2polssN  39520  3polN  39521  2pmaplubN  39531  paddunN  39532  poldmj1N  39533  pnonsingN  39538  ispsubcl2N  39552  psubclinN  39553  paddatclN  39554  polsubclN  39557  poml4N  39558  diaglbN  40660  diaintclN  40663  dibglbN  40771  dibintclN  40772  dihglblem2N  40899  dihglblem3N  40900  dihglblem4  40902  dihglbcpreN  40905  dihglblem6  40945  dihintcl  40949  dochval2  40957  dochcl  40958  dochvalr  40962  dochss  40970