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 37871
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 37868 . 2 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2 atllat 37808 . 2 (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
31, 2syl 17 1 (𝐾 ∈ HL → 𝐾 ∈ Lat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Latclat 18325  AtLatcal 37772  HLchlt 37858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-dm 5644  df-iota 6449  df-fv 6505  df-ov 7361  df-atl 37806  df-cvlat 37830  df-hlat 37859
This theorem is referenced by:  hllatd  37872  hlpos  37874  hlatjcl  37875  hlatjcom  37876  hlatjidm  37877  hlatjass  37878  hlatj32  37880  hlatj4  37882  hlatlej1  37883  atnlej1  37888  atnlej2  37889  hlateq  37908  hlrelat5N  37910  hlrelat2  37912  cvr2N  37920  cvrval5  37924  cvrexchlem  37928  cvrexch  37929  cvratlem  37930  cvrat  37931  cvrat2  37938  atcvrj2b  37941  atltcvr  37944  atlelt  37947  cvrat3  37951  cvrat4  37952  cvrat42  37953  2atjm  37954  3noncolr2  37958  3dimlem3OLDN  37971  3dimlem4OLDN  37974  1cvrat  37985  ps-1  37986  ps-2  37987  hlatexch3N  37989  3at  37999  llnneat  38023  lplni2  38046  2atnelpln  38053  lplnneat  38054  lplnnelln  38055  islpln2a  38057  2lplnmN  38068  2llnmj  38069  2llnm2N  38077  2llnm3N  38078  2llnm4  38079  2llnmeqat  38080  islvol5  38088  3atnelvolN  38095  lvolneatN  38097  lvolnelln  38098  lvolnelpln  38099  2lplnm2N  38130  2lplnmj  38131  pmap11  38271  isline3  38285  lncvrelatN  38290  2atm2atN  38294  2llnma1b  38295  2llnma3r  38297  paddasslem16  38344  paddass  38347  padd12N  38348  pmod2iN  38358  pmodN  38359  pmapjat1  38362  pmapjat2  38363  pmapjlln1  38364  hlmod1i  38365  atmod2i1  38370  atmod2i2  38371  atmod3i1  38373  atmod3i2  38374  atmod4i1  38375  atmod4i2  38376  llnexch2N  38379  polsubN  38416  paddunN  38436  pmapj2N  38438  pmapocjN  38439  psubclinN  38457  paddatclN  38458  linepsubclN  38460  lhpocnle  38525  lhpjat2  38530  lhpmcvr  38532  lhpm0atN  38538  lhpmatb  38540  trlval2  38672  trlcl  38673  trlle  38693  cdlemd1  38707  cdleme0cp  38723  cdleme0cq  38724  cdleme1b  38735  cdleme1  38736  cdleme2  38737  cdleme3b  38738  cdleme3c  38739  cdleme3e  38741  cdleme9b  38761  cdlemedb  38806  cdleme20zN  38810  cdleme19a  38812  cdlemf2  39071  tendoidcl  39278  dia1eldmN  39550  dialss  39555  dia1N  39562  diaglbN  39564  diaintclN  39567  docaclN  39633  doca2N  39635  djajN  39646  dibglbN  39675  dibintclN  39676  dihlsscpre  39743  dih2dimbALTN  39754  dih1  39795  dihglblem5apreN  39800  dihglblem5aN  39801  dihglblem2aN  39802  dihmeetcl  39854  dochvalr  39866  djhlj  39910
  Copyright terms: Public domain W3C validator