Theorem hlcvl 40114

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

Syntax hints:   → wi 4   ∈ wcel 2143  CLatccla 18555  OMLcoml 39930  CvLatclc 40020  HLchlt 40105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-hlat 40106

This theorem is referenced by:  hlatl  40115  hlexch1  40137  hlexch2  40138  hlexchb1  40139  hlexchb2  40140  hlsupr2  40142  hlexch3  40146  hlexch4N  40147  hlatexchb1  40148  hlatexchb2  40149  hlatexch1  40150  hlatexch2  40151  llnexchb2lem  40623  4atexlemkc  40813  4atex  40831  4atex3  40836  cdleme02N  40977  cdleme0ex2N  40979  cdleme0moN  40980  cdleme0nex  41045  cdleme20zN  41056  cdleme19a  41058  cdleme19d  41061  cdleme21a  41080  cdleme21b  41081  cdleme21c  41082  cdleme21ct  41084  cdleme22f  41101  cdleme22f2  41102  cdleme22g  41103  cdlemf1  41316