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

Theorem hlcvl 33286
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 33283 . 2  |-  ( K  e.  HL  ->  ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  CvLat
) )
21simp3d 1002 1  |-  ( K  e.  HL  ->  K  e.  CvLat )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1757   CLatccla 15365   OMLcoml 33102   CvLatclc 33192   HLchlt 33277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ral 2797  df-rex 2798  df-rab 2801  df-v 3056  df-dif 3415  df-un 3417  df-in 3419  df-ss 3426  df-nul 3722  df-if 3876  df-sn 3962  df-pr 3964  df-op 3968  df-uni 4176  df-br 4377  df-iota 5465  df-fv 5510  df-ov 6179  df-hlat 33278
This theorem is referenced by:  hlatl  33287  hlexch1  33308  hlexch2  33309  hlexchb1  33310  hlexchb2  33311  hlsupr2  33313  hlexch3  33317  hlexch4N  33318  hlatexchb1  33319  hlatexchb2  33320  hlatexch1  33321  hlatexch2  33322  llnexchb2lem  33794  4atexlemkc  33984  4atex  34002  4atex3  34007  cdleme02N  34148  cdleme0ex2N  34150  cdleme0moN  34151  cdleme0nex  34216  cdleme20zN  34227  cdleme20y  34228  cdleme19a  34229  cdleme19d  34232  cdleme21a  34251  cdleme21b  34252  cdleme21c  34253  cdleme21ct  34255  cdleme22f  34272  cdleme22f2  34273  cdleme22g  34274  cdlemf1  34487
  Copyright terms: Public domain W3C validator