Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hlcvl Structured version   Visualization version   GIF version

Theorem hlcvl 34161
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
StepHypRef Expression
1 hlomcmcv 34158 . 2 (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat))
21simp3d 1073 1 (𝐾 ∈ HL → 𝐾 ∈ CvLat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  CLatccla 17039  OMLcoml 33977  CvLatclc 34067  HLchlt 34152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5815  df-fv 5860  df-ov 6613  df-hlat 34153
This theorem is referenced by:  hlatl  34162  hlexch1  34183  hlexch2  34184  hlexchb1  34185  hlexchb2  34186  hlsupr2  34188  hlexch3  34192  hlexch4N  34193  hlatexchb1  34194  hlatexchb2  34195  hlatexch1  34196  hlatexch2  34197  llnexchb2lem  34669  4atexlemkc  34859  4atex  34877  4atex3  34882  cdleme02N  35024  cdleme0ex2N  35026  cdleme0moN  35027  cdleme0nex  35092  cdleme20zN  35103  cdleme20yOLD  35105  cdleme19a  35106  cdleme19d  35109  cdleme21a  35128  cdleme21b  35129  cdleme21c  35130  cdleme21ct  35132  cdleme22f  35149  cdleme22f2  35150  cdleme22g  35151  cdlemf1  35364
  Copyright terms: Public domain W3C validator