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

Theorem hlcvl 35481
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 35478 . 2  |-  ( K  e.  HL  ->  ( K  e.  OML  /\  K  e.  CLat  /\  K  e.  CvLat
) )
21simp3d 1008 1  |-  ( K  e.  HL  ->  K  e.  CvLat )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823   CLatccla 15936   OMLcoml 35297   CvLatclc 35387   HLchlt 35472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273  df-hlat 35473
This theorem is referenced by:  hlatl  35482  hlexch1  35503  hlexch2  35504  hlexchb1  35505  hlexchb2  35506  hlsupr2  35508  hlexch3  35512  hlexch4N  35513  hlatexchb1  35514  hlatexchb2  35515  hlatexch1  35516  hlatexch2  35517  llnexchb2lem  35989  4atexlemkc  36179  4atex  36197  4atex3  36202  cdleme02N  36344  cdleme0ex2N  36346  cdleme0moN  36347  cdleme0nex  36412  cdleme20zN  36423  cdleme20yOLD  36425  cdleme19a  36426  cdleme19d  36429  cdleme21a  36448  cdleme21b  36449  cdleme21c  36450  cdleme21ct  36452  cdleme22f  36469  cdleme22f2  36470  cdleme22g  36471  cdlemf1  36684
  Copyright terms: Public domain W3C validator