Theorem hlcvl 36655

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

Syntax hints:   → wi 4   ∈ wcel 2111  CLatccla 17709  OMLcoml 36471  CvLatclc 36561  HLchlt 36646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-hlat 36647

This theorem is referenced by:  hlatl  36656  hlexch1  36678  hlexch2  36679  hlexchb1  36680  hlexchb2  36681  hlsupr2  36683  hlexch3  36687  hlexch4N  36688  hlatexchb1  36689  hlatexchb2  36690  hlatexch1  36691  hlatexch2  36692  llnexchb2lem  37164  4atexlemkc  37354  4atex  37372  4atex3  37377  cdleme02N  37518  cdleme0ex2N  37520  cdleme0moN  37521  cdleme0nex  37586  cdleme20zN  37597  cdleme19a  37599  cdleme19d  37602  cdleme21a  37621  cdleme21b  37622  cdleme21c  37623  cdleme21ct  37625  cdleme22f  37642  cdleme22f2  37643  cdleme22g  37644  cdlemf1  37857