Theorem hlclat 36509

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

Syntax hints:   → wi 4   ∈ wcel 2114  CLatccla 17717  OMLcoml 36326  CvLatclc 36416  HLchlt 36501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159  df-hlat 36502

This theorem is referenced by:  hlomcmat  36516  glbconN  36528  pmaple  36912  pmapglbx  36920  polsubN  37058  2polvalN  37065  2polssN  37066  3polN  37067  2pmaplubN  37077  paddunN  37078  poldmj1N  37079  pnonsingN  37084  ispsubcl2N  37098  psubclinN  37099  paddatclN  37100  polsubclN  37103  poml4N  37104  diaglbN  38206  diaintclN  38209  dibglbN  38317  dibintclN  38318  dihglblem2N  38445  dihglblem3N  38446  dihglblem4  38448  dihglbcpreN  38451  dihglblem6  38491  dihintcl  38495  dochval2  38503  dochcl  38504  dochvalr  38508  dochss  38516