Theorem hlcvl 39404

Description: A Hilbert lattice is an atomic lattice with the covering property. (Contributed by NM, 5-Nov-2012.)

Assertion

Ref	Expression
hlcvl	⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat)

Proof of Theorem hlcvl

Step	Hyp	Ref	Expression
1		hlomcmcv 39401	. 2 ⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat))
2	1	simp3d 1144	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat)

Syntax hints:   → wi 4   ∈ wcel 2111  CLatccla 18404  OMLcoml 39220  CvLatclc 39310  HLchlt 39395

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-hlat 39396

This theorem is referenced by:  hlatl  39405  hlexch1  39427  hlexch2  39428  hlexchb1  39429  hlexchb2  39430  hlsupr2  39432  hlexch3  39436  hlexch4N  39437  hlatexchb1  39438  hlatexchb2  39439  hlatexch1  39440  hlatexch2  39441  llnexchb2lem  39913  4atexlemkc  40103  4atex  40121  4atex3  40126  cdleme02N  40267  cdleme0ex2N  40269  cdleme0moN  40270  cdleme0nex  40335  cdleme20zN  40346  cdleme19a  40348  cdleme19d  40351  cdleme21a  40370  cdleme21b  40371  cdleme21c  40372  cdleme21ct  40374  cdleme22f  40391  cdleme22f2  40392  cdleme22g  40393  cdlemf1  40606