Theorem hlclat 39314

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

Syntax hints:   → wi 4   ∈ wcel 2108  CLatccla 18568  OMLcoml 39131  CvLatclc 39221  HLchlt 39306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-hlat 39307

This theorem is referenced by:  hlomcmat  39321  glbconN  39333  glbconNOLD  39334  pmaple  39718  pmapglbx  39726  polsubN  39864  2polvalN  39871  2polssN  39872  3polN  39873  2pmaplubN  39883  paddunN  39884  poldmj1N  39885  pnonsingN  39890  ispsubcl2N  39904  psubclinN  39905  paddatclN  39906  polsubclN  39909  poml4N  39910  diaglbN  41012  diaintclN  41015  dibglbN  41123  dibintclN  41124  dihglblem2N  41251  dihglblem3N  41252  dihglblem4  41254  dihglbcpreN  41257  dihglblem6  41297  dihintcl  41301  dochval2  41309  dochcl  41310  dochvalr  41314  dochss  41322