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 35168
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 35165 . 2 (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat))
21simp3d 1138 1 (𝐾 ∈ HL → 𝐾 ∈ CvLat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2145  CLatccla 17315  OMLcoml 34984  CvLatclc 35074  HLchlt 35159
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-iota 5993  df-fv 6038  df-ov 6799  df-hlat 35160
This theorem is referenced by:  hlatl  35169  hlexch1  35191  hlexch2  35192  hlexchb1  35193  hlexchb2  35194  hlsupr2  35196  hlexch3  35200  hlexch4N  35201  hlatexchb1  35202  hlatexchb2  35203  hlatexch1  35204  hlatexch2  35205  llnexchb2lem  35677  4atexlemkc  35867  4atex  35885  4atex3  35890  cdleme02N  36032  cdleme0ex2N  36034  cdleme0moN  36035  cdleme0nex  36100  cdleme20zN  36111  cdleme19a  36113  cdleme19d  36116  cdleme21a  36135  cdleme21b  36136  cdleme21c  36137  cdleme21ct  36139  cdleme22f  36156  cdleme22f2  36157  cdleme22g  36158  cdlemf1  36371
  Copyright terms: Public domain W3C validator