Theorem hlclat 40383

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  CLatccla 18652  OMLcoml 40200  CvLatclc 40290  HLchlt 40375

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415  df-hlat 40376

This theorem is used by:  hlomcmat  40390  glbconN  40402  pmaple  40786  pmapglbx  40794  polsubN  40932  2polvalN  40939  2polssN  40940  3polN  40941  2pmaplubN  40951  paddunN  40952  poldmj1N  40953  pnonsingN  40958  ispsubcl2N  40972  psubclinN  40973  paddatclN  40974  polsubclN  40977  poml4N  40978  diaglbN  42080  diaintclN  42083  dibglbN  42191  dibintclN  42192  dihglblem2N  42319  dihglblem3N  42320  dihglblem4  42322  dihglbcpreN  42325  dihglblem6  42365  dihintcl  42369  dochval2  42377  dochcl  42378  dochvalr  42382  dochss  42390