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 35162
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 35159 . 2 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2 atllat 35099 . 2 (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
31, 2syl 17 1 (𝐾 ∈ HL → 𝐾 ∈ Lat)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157  Latclat 17270  AtLatcal 35063  HLchlt 35149
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-dm 5334  df-iota 6074  df-fv 6119  df-ov 6887  df-atl 35097  df-cvlat 35121  df-hlat 35150
This theorem is referenced by:  hllatd  35163  hlpos  35165  hlatjcl  35166  hlatjcom  35167  hlatjidm  35168  hlatjass  35169  hlatj32  35171  hlatj4  35173  hlatlej1  35174  atnlej1  35178  atnlej2  35179  hlateq  35198  hlrelat5N  35200  hlrelat2  35202  cvr2N  35210  cvrval5  35214  cvrexchlem  35218  cvrexch  35219  cvratlem  35220  cvrat  35221  cvrat2  35228  atcvrj2b  35231  atltcvr  35234  atlelt  35237  cvrat3  35241  cvrat4  35242  cvrat42  35243  2atjm  35244  3noncolr2  35248  3dimlem3OLDN  35261  3dimlem4OLDN  35264  1cvrat  35275  ps-1  35276  ps-2  35277  hlatexch3N  35279  3at  35289  llnneat  35313  lplni2  35336  2atnelpln  35343  lplnneat  35344  lplnnelln  35345  islpln2a  35347  2lplnmN  35358  2llnmj  35359  2llnm2N  35367  2llnm3N  35368  2llnm4  35369  2llnmeqat  35370  islvol5  35378  3atnelvolN  35385  lvolneatN  35387  lvolnelln  35388  lvolnelpln  35389  2lplnm2N  35420  2lplnmj  35421  pmap11  35561  isline3  35575  lncvrelatN  35580  2atm2atN  35584  2llnma1b  35585  2llnma3r  35587  paddasslem16  35634  paddass  35637  padd12N  35638  pmod2iN  35648  pmodN  35649  pmapjat1  35652  pmapjat2  35653  pmapjlln1  35654  hlmod1i  35655  atmod2i1  35660  atmod2i2  35661  atmod3i1  35663  atmod3i2  35664  atmod4i1  35665  atmod4i2  35666  llnexch2N  35669  polsubN  35706  paddunN  35726  pmapj2N  35728  pmapocjN  35729  psubclinN  35747  paddatclN  35748  linepsubclN  35750  lhpocnle  35815  lhpjat2  35820  lhpmcvr  35822  lhpm0atN  35828  lhpmatb  35830  trlval2  35962  trlcl  35963  trlle  35983  cdlemd1  35997  cdleme0cp  36013  cdleme0cq  36014  cdleme1b  36025  cdleme1  36026  cdleme2  36027  cdleme3b  36028  cdleme3c  36029  cdleme3e  36031  cdleme9b  36051  cdlemedb  36096  cdleme20zN  36100  cdleme19a  36102  cdlemf2  36361  tendoidcl  36568  dia1eldmN  36840  dialss  36845  dia1N  36852  diaglbN  36854  diaintclN  36857  docaclN  36923  doca2N  36925  djajN  36936  dibglbN  36965  dibintclN  36966  dihlsscpre  37033  dih2dimbALTN  37044  dih1  37085  dihglblem5apreN  37090  dihglblem5aN  37091  dihglblem2aN  37092  dihmeetcl  37144  dochvalr  37156  djhlj  37200
  Copyright terms: Public domain W3C validator