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

Theorem hlcvl 29367
Description: A Hilbert lattice is an atomic lattice with the covering property. (Contributed by NM, 5-Nov-2012.)
Assertion
Ref Expression
hlcvl  |-  ( K  e.  HL  ->  K  e.  CvLat )

Proof of Theorem hlcvl
StepHypRef Expression
1 hlomcmcv 29364 . 2  |-  ( K  e.  HL  ->  ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  CvLat
) )
21simp3d 969 1  |-  ( K  e.  HL  ->  K  e.  CvLat )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1701   CLatccla 14262   OMLcoml 29183   CvLatclc 29273   HLchlt 29358
This theorem is referenced by:  hlatl  29368  hlexch1  29389  hlexch2  29390  hlexchb1  29391  hlexchb2  29392  hlsupr2  29394  hlexch3  29398  hlexch4N  29399  hlatexchb1  29400  hlatexchb2  29401  hlatexch1  29402  hlatexch2  29403  llnexchb2lem  29875  4atexlemkc  30065  4atex  30083  4atex3  30088  cdleme02N  30229  cdleme0ex2N  30231  cdleme0moN  30232  cdleme0nex  30297  cdleme20zN  30308  cdleme20y  30309  cdleme19a  30310  cdleme19d  30313  cdleme21a  30332  cdleme21b  30333  cdleme21c  30334  cdleme21ct  30336  cdleme22f  30353  cdleme22f2  30354  cdleme22g  30355  cdlemf1  30568
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-iota 5256  df-fv 5300  df-ov 5903  df-hlat 29359
  Copyright terms: Public domain W3C validator