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

Theorem hllat 36605
Description: A Hilbert lattice is a lattice. (Contributed by NM, 20-Oct-2011.)
Assertion
Ref Expression
hllat (𝐾 ∈ HL → 𝐾 ∈ Lat)

Proof of Theorem hllat
StepHypRef Expression
1 hlatl 36602 . 2 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2 atllat 36542 . 2 (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
31, 2syl 17 1 (𝐾 ∈ HL → 𝐾 ∈ Lat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  Latclat 17658  AtLatcal 36506  HLchlt 36592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3483  df-un 3925  df-in 3927  df-ss 3937  df-sn 4552  df-pr 4554  df-op 4558  df-uni 4826  df-br 5054  df-dm 5553  df-iota 6303  df-fv 6352  df-ov 7153  df-atl 36540  df-cvlat 36564  df-hlat 36593
This theorem is referenced by:  hllatd  36606  hlpos  36608  hlatjcl  36609  hlatjcom  36610  hlatjidm  36611  hlatjass  36612  hlatj32  36614  hlatj4  36616  hlatlej1  36617  atnlej1  36621  atnlej2  36622  hlateq  36641  hlrelat5N  36643  hlrelat2  36645  cvr2N  36653  cvrval5  36657  cvrexchlem  36661  cvrexch  36662  cvratlem  36663  cvrat  36664  cvrat2  36671  atcvrj2b  36674  atltcvr  36677  atlelt  36680  cvrat3  36684  cvrat4  36685  cvrat42  36686  2atjm  36687  3noncolr2  36691  3dimlem3OLDN  36704  3dimlem4OLDN  36707  1cvrat  36718  ps-1  36719  ps-2  36720  hlatexch3N  36722  3at  36732  llnneat  36756  lplni2  36779  2atnelpln  36786  lplnneat  36787  lplnnelln  36788  islpln2a  36790  2lplnmN  36801  2llnmj  36802  2llnm2N  36810  2llnm3N  36811  2llnm4  36812  2llnmeqat  36813  islvol5  36821  3atnelvolN  36828  lvolneatN  36830  lvolnelln  36831  lvolnelpln  36832  2lplnm2N  36863  2lplnmj  36864  pmap11  37004  isline3  37018  lncvrelatN  37023  2atm2atN  37027  2llnma1b  37028  2llnma3r  37030  paddasslem16  37077  paddass  37080  padd12N  37081  pmod2iN  37091  pmodN  37092  pmapjat1  37095  pmapjat2  37096  pmapjlln1  37097  hlmod1i  37098  atmod2i1  37103  atmod2i2  37104  atmod3i1  37106  atmod3i2  37107  atmod4i1  37108  atmod4i2  37109  llnexch2N  37112  polsubN  37149  paddunN  37169  pmapj2N  37171  pmapocjN  37172  psubclinN  37190  paddatclN  37191  linepsubclN  37193  lhpocnle  37258  lhpjat2  37263  lhpmcvr  37265  lhpm0atN  37271  lhpmatb  37273  trlval2  37405  trlcl  37406  trlle  37426  cdlemd1  37440  cdleme0cp  37456  cdleme0cq  37457  cdleme1b  37468  cdleme1  37469  cdleme2  37470  cdleme3b  37471  cdleme3c  37472  cdleme3e  37474  cdleme9b  37494  cdlemedb  37539  cdleme20zN  37543  cdleme19a  37545  cdlemf2  37804  tendoidcl  38011  dia1eldmN  38283  dialss  38288  dia1N  38295  diaglbN  38297  diaintclN  38300  docaclN  38366  doca2N  38368  djajN  38379  dibglbN  38408  dibintclN  38409  dihlsscpre  38476  dih2dimbALTN  38487  dih1  38528  dihglblem5apreN  38533  dihglblem5aN  38534  dihglblem2aN  38535  dihmeetcl  38587  dochvalr  38599  djhlj  38643
  Copyright terms: Public domain W3C validator