Theorem hlcvl 39359

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

Syntax hints:   → wi 4   ∈ wcel 2109  CLatccla 18464  OMLcoml 39175  CvLatclc 39265  HLchlt 39350

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-hlat 39351

This theorem is referenced by:  hlatl  39360  hlexch1  39383  hlexch2  39384  hlexchb1  39385  hlexchb2  39386  hlsupr2  39388  hlexch3  39392  hlexch4N  39393  hlatexchb1  39394  hlatexchb2  39395  hlatexch1  39396  hlatexch2  39397  llnexchb2lem  39869  4atexlemkc  40059  4atex  40077  4atex3  40082  cdleme02N  40223  cdleme0ex2N  40225  cdleme0moN  40226  cdleme0nex  40291  cdleme20zN  40302  cdleme19a  40304  cdleme19d  40307  cdleme21a  40326  cdleme21b  40327  cdleme21c  40328  cdleme21ct  40330  cdleme22f  40347  cdleme22f2  40348  cdleme22g  40349  cdlemf1  40562