Theorem hlcvl 36985

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

Syntax hints:   → wi 4   ∈ wcel 2113  CLatccla 17826  OMLcoml 36801  CvLatclc 36891  HLchlt 36976

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 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3399  df-un 3846  df-in 3848  df-ss 3858  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-br 5028  df-iota 6291  df-fv 6341  df-ov 7167  df-hlat 36977

This theorem is referenced by:  hlatl  36986  hlexch1  37008  hlexch2  37009  hlexchb1  37010  hlexchb2  37011  hlsupr2  37013  hlexch3  37017  hlexch4N  37018  hlatexchb1  37019  hlatexchb2  37020  hlatexch1  37021  hlatexch2  37022  llnexchb2lem  37494  4atexlemkc  37684  4atex  37702  4atex3  37707  cdleme02N  37848  cdleme0ex2N  37850  cdleme0moN  37851  cdleme0nex  37916  cdleme20zN  37927  cdleme19a  37929  cdleme19d  37932  cdleme21a  37951  cdleme21b  37952  cdleme21c  37953  cdleme21ct  37955  cdleme22f  37972  cdleme22f2  37973  cdleme22g  37974  cdlemf1  38187