Theorem hllat 38233

Description: A Hilbert lattice is a lattice. (Contributed by NM, 20-Oct-2011.)

Assertion

Ref	Expression
hllat	⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)

Proof of Theorem hllat

Step	Hyp	Ref	Expression
1		hlatl 38230	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2		atllat 38170	. 2 ⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)

Syntax hints:   → wi 4   ∈ wcel 2107  Latclat 18384  AtLatcal 38134  HLchlt 38220

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 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-dm 5687  df-iota 6496  df-fv 6552  df-ov 7412  df-atl 38168  df-cvlat 38192  df-hlat 38221

This theorem is referenced by:  hllatd  38234  hlpos  38236  hlatjcl  38237  hlatjcom  38238  hlatjidm  38239  hlatjass  38240  hlatj32  38242  hlatj4  38244  hlatlej1  38245  atnlej1  38250  atnlej2  38251  hlateq  38270  hlrelat5N  38272  hlrelat2  38274  cvr2N  38282  cvrval5  38286  cvrexchlem  38290  cvrexch  38291  cvratlem  38292  cvrat  38293  cvrat2  38300  atcvrj2b  38303  atltcvr  38306  atlelt  38309  cvrat3  38313  cvrat4  38314  cvrat42  38315  2atjm  38316  3noncolr2  38320  3dimlem3OLDN  38333  3dimlem4OLDN  38336  1cvrat  38347  ps-1  38348  ps-2  38349  hlatexch3N  38351  3at  38361  llnneat  38385  lplni2  38408  2atnelpln  38415  lplnneat  38416  lplnnelln  38417  islpln2a  38419  2lplnmN  38430  2llnmj  38431  2llnm2N  38439  2llnm3N  38440  2llnm4  38441  2llnmeqat  38442  islvol5  38450  3atnelvolN  38457  lvolneatN  38459  lvolnelln  38460  lvolnelpln  38461  2lplnm2N  38492  2lplnmj  38493  pmap11  38633  isline3  38647  lncvrelatN  38652  2atm2atN  38656  2llnma1b  38657  2llnma3r  38659  paddasslem16  38706  paddass  38709  padd12N  38710  pmod2iN  38720  pmodN  38721  pmapjat1  38724  pmapjat2  38725  pmapjlln1  38726  hlmod1i  38727  atmod2i1  38732  atmod2i2  38733  atmod3i1  38735  atmod3i2  38736  atmod4i1  38737  atmod4i2  38738  llnexch2N  38741  polsubN  38778  paddunN  38798  pmapj2N  38800  pmapocjN  38801  psubclinN  38819  paddatclN  38820  linepsubclN  38822  lhpocnle  38887  lhpjat2  38892  lhpmcvr  38894  lhpm0atN  38900  lhpmatb  38902  trlval2  39034  trlcl  39035  trlle  39055  cdlemd1  39069  cdleme0cp  39085  cdleme0cq  39086  cdleme1b  39097  cdleme1  39098  cdleme2  39099  cdleme3b  39100  cdleme3c  39101  cdleme3e  39103  cdleme9b  39123  cdlemedb  39168  cdleme20zN  39172  cdleme19a  39174  cdlemf2  39433  tendoidcl  39640  dia1eldmN  39912  dialss  39917  dia1N  39924  diaglbN  39926  diaintclN  39929  docaclN  39995  doca2N  39997  djajN  40008  dibglbN  40037  dibintclN  40038  dihlsscpre  40105  dih2dimbALTN  40116  dih1  40157  dihglblem5apreN  40162  dihglblem5aN  40163  dihglblem2aN  40164  dihmeetcl  40216  dochvalr  40228  djhlj  40272