Theorem hlcvl 39306

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

Syntax hints:   → wi 4   ∈ wcel 2107  CLatccla 18495  OMLcoml 39122  CvLatclc 39212  HLchlt 39297

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4882  df-br 5118  df-iota 6481  df-fv 6536  df-ov 7403  df-hlat 39298

This theorem is referenced by:  hlatl  39307  hlexch1  39330  hlexch2  39331  hlexchb1  39332  hlexchb2  39333  hlsupr2  39335  hlexch3  39339  hlexch4N  39340  hlatexchb1  39341  hlatexchb2  39342  hlatexch1  39343  hlatexch2  39344  llnexchb2lem  39816  4atexlemkc  40006  4atex  40024  4atex3  40029  cdleme02N  40170  cdleme0ex2N  40172  cdleme0moN  40173  cdleme0nex  40238  cdleme20zN  40249  cdleme19a  40251  cdleme19d  40254  cdleme21a  40273  cdleme21b  40274  cdleme21c  40275  cdleme21ct  40277  cdleme22f  40294  cdleme22f2  40295  cdleme22g  40296  cdlemf1  40509