Theorem hlcvl 40417

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  CLatccla 18672  OMLcoml 40233  CvLatclc 40323  HLchlt 40408

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-hlat 40409

This theorem is used by:  hlatl  40418  hlexch1  40440  hlexch2  40441  hlexchb1  40442  hlexchb2  40443  hlsupr2  40445  hlexch3  40449  hlexch4N  40450  hlatexchb1  40451  hlatexchb2  40452  hlatexch1  40453  hlatexch2  40454  llnexchb2lem  40926  4atexlemkc  41116  4atex  41134  4atex3  41139  cdleme02N  41280  cdleme0ex2N  41282  cdleme0moN  41283  cdleme0nex  41348  cdleme20zN  41359  cdleme19a  41361  cdleme19d  41364  cdleme21a  41383  cdleme21b  41384  cdleme21c  41385  cdleme21ct  41387  cdleme22f  41404  cdleme22f2  41405  cdleme22g  41406  cdlemf1  41619