Theorem hlcvl 39340

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

Syntax hints:   → wi 4   ∈ wcel 2109  CLatccla 18422  OMLcoml 39156  CvLatclc 39246  HLchlt 39331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-hlat 39332

This theorem is referenced by:  hlatl  39341  hlexch1  39364  hlexch2  39365  hlexchb1  39366  hlexchb2  39367  hlsupr2  39369  hlexch3  39373  hlexch4N  39374  hlatexchb1  39375  hlatexchb2  39376  hlatexch1  39377  hlatexch2  39378  llnexchb2lem  39850  4atexlemkc  40040  4atex  40058  4atex3  40063  cdleme02N  40204  cdleme0ex2N  40206  cdleme0moN  40207  cdleme0nex  40272  cdleme20zN  40283  cdleme19a  40285  cdleme19d  40288  cdleme21a  40307  cdleme21b  40308  cdleme21c  40309  cdleme21ct  40311  cdleme22f  40328  cdleme22f2  40329  cdleme22g  40330  cdlemf1  40543