Theorem hlcvl 39531

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

Syntax hints:   → wi 4   ∈ wcel 2113  CLatccla 18412  OMLcoml 39347  CvLatclc 39437  HLchlt 39522

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358  df-hlat 39523

This theorem is referenced by:  hlatl  39532  hlexch1  39554  hlexch2  39555  hlexchb1  39556  hlexchb2  39557  hlsupr2  39559  hlexch3  39563  hlexch4N  39564  hlatexchb1  39565  hlatexchb2  39566  hlatexch1  39567  hlatexch2  39568  llnexchb2lem  40040  4atexlemkc  40230  4atex  40248  4atex3  40253  cdleme02N  40394  cdleme0ex2N  40396  cdleme0moN  40397  cdleme0nex  40462  cdleme20zN  40473  cdleme19a  40475  cdleme19d  40478  cdleme21a  40497  cdleme21b  40498  cdleme21c  40499  cdleme21ct  40501  cdleme22f  40518  cdleme22f2  40519  cdleme22g  40520  cdlemf1  40733