Theorem hlcvl 37373

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

Syntax hints:   → wi 4   ∈ wcel 2106  CLatccla 18216  OMLcoml 37189  CvLatclc 37279  HLchlt 37364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278  df-hlat 37365

This theorem is referenced by:  hlatl  37374  hlexch1  37396  hlexch2  37397  hlexchb1  37398  hlexchb2  37399  hlsupr2  37401  hlexch3  37405  hlexch4N  37406  hlatexchb1  37407  hlatexchb2  37408  hlatexch1  37409  hlatexch2  37410  llnexchb2lem  37882  4atexlemkc  38072  4atex  38090  4atex3  38095  cdleme02N  38236  cdleme0ex2N  38238  cdleme0moN  38239  cdleme0nex  38304  cdleme20zN  38315  cdleme19a  38317  cdleme19d  38320  cdleme21a  38339  cdleme21b  38340  cdleme21c  38341  cdleme21ct  38343  cdleme22f  38360  cdleme22f2  38361  cdleme22g  38362  cdlemf1  38575