Theorem hlcvl 39732

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 39729	. 2 ⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat))
2	1	simp3d 1145	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat)

Syntax hints:   → wi 4   ∈ wcel 2114  CLatccla 18433  OMLcoml 39548  CvLatclc 39638  HLchlt 39723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-hlat 39724

This theorem is referenced by:  hlatl  39733  hlexch1  39755  hlexch2  39756  hlexchb1  39757  hlexchb2  39758  hlsupr2  39760  hlexch3  39764  hlexch4N  39765  hlatexchb1  39766  hlatexchb2  39767  hlatexch1  39768  hlatexch2  39769  llnexchb2lem  40241  4atexlemkc  40431  4atex  40449  4atex3  40454  cdleme02N  40595  cdleme0ex2N  40597  cdleme0moN  40598  cdleme0nex  40663  cdleme20zN  40674  cdleme19a  40676  cdleme19d  40679  cdleme21a  40698  cdleme21b  40699  cdleme21c  40700  cdleme21ct  40702  cdleme22f  40719  cdleme22f2  40720  cdleme22g  40721  cdlemf1  40934