Theorem hlcvl 40396

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  CLatccla 18665  OMLcoml 40212  CvLatclc 40302  HLchlt 40387

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545  df-ov 7421  df-hlat 40388

This theorem is used by:  hlatl  40397  hlexch1  40419  hlexch2  40420  hlexchb1  40421  hlexchb2  40422  hlsupr2  40424  hlexch3  40428  hlexch4N  40429  hlatexchb1  40430  hlatexchb2  40431  hlatexch1  40432  hlatexch2  40433  llnexchb2lem  40905  4atexlemkc  41095  4atex  41113  4atex3  41118  cdleme02N  41259  cdleme0ex2N  41261  cdleme0moN  41262  cdleme0nex  41327  cdleme20zN  41338  cdleme19a  41340  cdleme19d  41343  cdleme21a  41362  cdleme21b  41363  cdleme21c  41364  cdleme21ct  41366  cdleme22f  41383  cdleme22f2  41384  cdleme22g  41385  cdlemf1  41598