Theorem hlclat 39614

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

Syntax hints:   → wi 4   ∈ wcel 2113  CLatccla 18421  OMLcoml 39431  CvLatclc 39521  HLchlt 39606

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-hlat 39607

This theorem is referenced by:  hlomcmat  39621  glbconN  39633  pmaple  40017  pmapglbx  40025  polsubN  40163  2polvalN  40170  2polssN  40171  3polN  40172  2pmaplubN  40182  paddunN  40183  poldmj1N  40184  pnonsingN  40189  ispsubcl2N  40203  psubclinN  40204  paddatclN  40205  polsubclN  40208  poml4N  40209  diaglbN  41311  diaintclN  41314  dibglbN  41422  dibintclN  41423  dihglblem2N  41550  dihglblem3N  41551  dihglblem4  41553  dihglbcpreN  41556  dihglblem6  41596  dihintcl  41600  dochval2  41608  dochcl  41609  dochvalr  41613  dochss  41621