Theorem hlcvl 39619

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

Syntax hints:   → wi 4   ∈ wcel 2113  CLatccla 18421  OMLcoml 39435  CvLatclc 39525  HLchlt 39610

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-hlat 39611

This theorem is referenced by:  hlatl  39620  hlexch1  39642  hlexch2  39643  hlexchb1  39644  hlexchb2  39645  hlsupr2  39647  hlexch3  39651  hlexch4N  39652  hlatexchb1  39653  hlatexchb2  39654  hlatexch1  39655  hlatexch2  39656  llnexchb2lem  40128  4atexlemkc  40318  4atex  40336  4atex3  40341  cdleme02N  40482  cdleme0ex2N  40484  cdleme0moN  40485  cdleme0nex  40550  cdleme20zN  40561  cdleme19a  40563  cdleme19d  40566  cdleme21a  40585  cdleme21b  40586  cdleme21c  40587  cdleme21ct  40589  cdleme22f  40606  cdleme22f2  40607  cdleme22g  40608  cdlemf1  40821