Theorem hlcvl 39382

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

Syntax hints:   → wi 4   ∈ wcel 2109  CLatccla 18513  OMLcoml 39198  CvLatclc 39288  HLchlt 39373

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-hlat 39374

This theorem is referenced by:  hlatl  39383  hlexch1  39406  hlexch2  39407  hlexchb1  39408  hlexchb2  39409  hlsupr2  39411  hlexch3  39415  hlexch4N  39416  hlatexchb1  39417  hlatexchb2  39418  hlatexch1  39419  hlatexch2  39420  llnexchb2lem  39892  4atexlemkc  40082  4atex  40100  4atex3  40105  cdleme02N  40246  cdleme0ex2N  40248  cdleme0moN  40249  cdleme0nex  40314  cdleme20zN  40325  cdleme19a  40327  cdleme19d  40330  cdleme21a  40349  cdleme21b  40350  cdleme21c  40351  cdleme21ct  40353  cdleme22f  40370  cdleme22f2  40371  cdleme22g  40372  cdlemf1  40585