Theorem hlcvl 40166

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  CLatccla 18571  OMLcoml 39982  CvLatclc 40072  HLchlt 40157

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7419  df-hlat 40158

This theorem is used by:  hlatl  40167  hlexch1  40189  hlexch2  40190  hlexchb1  40191  hlexchb2  40192  hlsupr2  40194  hlexch3  40198  hlexch4N  40199  hlatexchb1  40200  hlatexchb2  40201  hlatexch1  40202  hlatexch2  40203  llnexchb2lem  40675  4atexlemkc  40865  4atex  40883  4atex3  40888  cdleme02N  41029  cdleme0ex2N  41031  cdleme0moN  41032  cdleme0nex  41097  cdleme20zN  41108  cdleme19a  41110  cdleme19d  41113  cdleme21a  41132  cdleme21b  41133  cdleme21c  41134  cdleme21ct  41136  cdleme22f  41153  cdleme22f2  41154  cdleme22g  41155  cdlemf1  41368