Theorem hlcvl 40018

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

Syntax hints:   → wi 4   ∈ wcel 2149  CLatccla 18550  OMLcoml 39834  CvLatclc 39924  HLchlt 40009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-iota 6489  df-fv 6541  df-ov 7411  df-hlat 40010

This theorem is referenced by:  hlatl  40019  hlexch1  40041  hlexch2  40042  hlexchb1  40043  hlexchb2  40044  hlsupr2  40046  hlexch3  40050  hlexch4N  40051  hlatexchb1  40052  hlatexchb2  40053  hlatexch1  40054  hlatexch2  40055  llnexchb2lem  40527  4atexlemkc  40717  4atex  40735  4atex3  40740  cdleme02N  40881  cdleme0ex2N  40883  cdleme0moN  40884  cdleme0nex  40949  cdleme20zN  40960  cdleme19a  40962  cdleme19d  40965  cdleme21a  40984  cdleme21b  40985  cdleme21c  40986  cdleme21ct  40988  cdleme22f  41005  cdleme22f2  41006  cdleme22g  41007  cdlemf1  41220