Theorem hlcvl 39944

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

Syntax hints:   → wi 4   ∈ wcel 2141  CLatccla 18521  OMLcoml 39760  CvLatclc 39850  HLchlt 39935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6472  df-fv 6524  df-ov 7394  df-hlat 39936

This theorem is referenced by:  hlatl  39945  hlexch1  39967  hlexch2  39968  hlexchb1  39969  hlexchb2  39970  hlsupr2  39972  hlexch3  39976  hlexch4N  39977  hlatexchb1  39978  hlatexchb2  39979  hlatexch1  39980  hlatexch2  39981  llnexchb2lem  40453  4atexlemkc  40643  4atex  40661  4atex3  40666  cdleme02N  40807  cdleme0ex2N  40809  cdleme0moN  40810  cdleme0nex  40875  cdleme20zN  40886  cdleme19a  40888  cdleme19d  40891  cdleme21a  40910  cdleme21b  40911  cdleme21c  40912  cdleme21ct  40914  cdleme22f  40931  cdleme22f2  40932  cdleme22g  40933  cdlemf1  41146