Theorem hllat 39329

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 39326	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2		atllat 39266	. 2 ⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)

Syntax hints:   → wi 4   ∈ wcel 2109  Latclat 18366  AtLatcal 39230  HLchlt 39316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-dm 5641  df-iota 6452  df-fv 6507  df-ov 7372  df-atl 39264  df-cvlat 39288  df-hlat 39317

This theorem is referenced by:  hllatd  39330  hlpos  39332  hlatjcl  39333  hlatjcom  39334  hlatjidm  39335  hlatjass  39336  hlatj32  39338  hlatj4  39340  hlatlej1  39341  atnlej1  39346  atnlej2  39347  hlateq  39366  hlrelat5N  39368  hlrelat2  39370  cvr2N  39378  cvrval5  39382  cvrexchlem  39386  cvrexch  39387  cvratlem  39388  cvrat  39389  cvrat2  39396  atcvrj2b  39399  atltcvr  39402  atlelt  39405  cvrat3  39409  cvrat4  39410  cvrat42  39411  2atjm  39412  3noncolr2  39416  3dimlem3OLDN  39429  3dimlem4OLDN  39432  1cvrat  39443  ps-1  39444  ps-2  39445  hlatexch3N  39447  3at  39457  llnneat  39481  lplni2  39504  2atnelpln  39511  lplnneat  39512  lplnnelln  39513  islpln2a  39515  2lplnmN  39526  2llnmj  39527  2llnm2N  39535  2llnm3N  39536  2llnm4  39537  2llnmeqat  39538  islvol5  39546  3atnelvolN  39553  lvolneatN  39555  lvolnelln  39556  lvolnelpln  39557  2lplnm2N  39588  2lplnmj  39589  pmap11  39729  isline3  39743  lncvrelatN  39748  2atm2atN  39752  2llnma1b  39753  2llnma3r  39755  paddasslem16  39802  paddass  39805  padd12N  39806  pmod2iN  39816  pmodN  39817  pmapjat1  39820  pmapjat2  39821  pmapjlln1  39822  hlmod1i  39823  atmod2i1  39828  atmod2i2  39829  atmod3i1  39831  atmod3i2  39832  atmod4i1  39833  atmod4i2  39834  llnexch2N  39837  polsubN  39874  paddunN  39894  pmapj2N  39896  pmapocjN  39897  psubclinN  39915  paddatclN  39916  linepsubclN  39918  lhpocnle  39983  lhpjat2  39988  lhpmcvr  39990  lhpm0atN  39996  lhpmatb  39998  trlval2  40130  trlcl  40131  trlle  40151  cdlemd1  40165  cdleme0cp  40181  cdleme0cq  40182  cdleme1b  40193  cdleme1  40194  cdleme2  40195  cdleme3b  40196  cdleme3c  40197  cdleme3e  40199  cdleme9b  40219  cdlemedb  40264  cdleme20zN  40268  cdleme19a  40270  cdlemf2  40529  tendoidcl  40736  dia1eldmN  41008  dialss  41013  dia1N  41020  diaglbN  41022  diaintclN  41025  docaclN  41091  doca2N  41093  djajN  41104  dibglbN  41133  dibintclN  41134  dihlsscpre  41201  dih2dimbALTN  41212  dih1  41253  dihglblem5apreN  41258  dihglblem5aN  41259  dihglblem2aN  41260  dihmeetcl  41312  dochvalr  41324  djhlj  41368