Theorem hlcvl 39851

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

Syntax hints:   → wi 4   ∈ wcel 2119  CLatccla 18455  OMLcoml 39667  CvLatclc 39757  HLchlt 39842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359  df-hlat 39843

This theorem is referenced by:  hlatl  39852  hlexch1  39874  hlexch2  39875  hlexchb1  39876  hlexchb2  39877  hlsupr2  39879  hlexch3  39883  hlexch4N  39884  hlatexchb1  39885  hlatexchb2  39886  hlatexch1  39887  hlatexch2  39888  llnexchb2lem  40360  4atexlemkc  40550  4atex  40568  4atex3  40573  cdleme02N  40714  cdleme0ex2N  40716  cdleme0moN  40717  cdleme0nex  40782  cdleme20zN  40793  cdleme19a  40795  cdleme19d  40798  cdleme21a  40817  cdleme21b  40818  cdleme21c  40819  cdleme21ct  40821  cdleme22f  40838  cdleme22f2  40839  cdleme22g  40840  cdlemf1  41053