Theorem hllat 39356

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

Syntax hints:   → wi 4   ∈ wcel 2109  Latclat 18390  AtLatcal 39257  HLchlt 39343

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-dm 5648  df-iota 6464  df-fv 6519  df-ov 7390  df-atl 39291  df-cvlat 39315  df-hlat 39344

This theorem is referenced by:  hllatd  39357  hlpos  39359  hlatjcl  39360  hlatjcom  39361  hlatjidm  39362  hlatjass  39363  hlatj32  39365  hlatj4  39367  hlatlej1  39368  atnlej1  39373  atnlej2  39374  hlateq  39393  hlrelat5N  39395  hlrelat2  39397  cvr2N  39405  cvrval5  39409  cvrexchlem  39413  cvrexch  39414  cvratlem  39415  cvrat  39416  cvrat2  39423  atcvrj2b  39426  atltcvr  39429  atlelt  39432  cvrat3  39436  cvrat4  39437  cvrat42  39438  2atjm  39439  3noncolr2  39443  3dimlem3OLDN  39456  3dimlem4OLDN  39459  1cvrat  39470  ps-1  39471  ps-2  39472  hlatexch3N  39474  3at  39484  llnneat  39508  lplni2  39531  2atnelpln  39538  lplnneat  39539  lplnnelln  39540  islpln2a  39542  2lplnmN  39553  2llnmj  39554  2llnm2N  39562  2llnm3N  39563  2llnm4  39564  2llnmeqat  39565  islvol5  39573  3atnelvolN  39580  lvolneatN  39582  lvolnelln  39583  lvolnelpln  39584  2lplnm2N  39615  2lplnmj  39616  pmap11  39756  isline3  39770  lncvrelatN  39775  2atm2atN  39779  2llnma1b  39780  2llnma3r  39782  paddasslem16  39829  paddass  39832  padd12N  39833  pmod2iN  39843  pmodN  39844  pmapjat1  39847  pmapjat2  39848  pmapjlln1  39849  hlmod1i  39850  atmod2i1  39855  atmod2i2  39856  atmod3i1  39858  atmod3i2  39859  atmod4i1  39860  atmod4i2  39861  llnexch2N  39864  polsubN  39901  paddunN  39921  pmapj2N  39923  pmapocjN  39924  psubclinN  39942  paddatclN  39943  linepsubclN  39945  lhpocnle  40010  lhpjat2  40015  lhpmcvr  40017  lhpm0atN  40023  lhpmatb  40025  trlval2  40157  trlcl  40158  trlle  40178  cdlemd1  40192  cdleme0cp  40208  cdleme0cq  40209  cdleme1b  40220  cdleme1  40221  cdleme2  40222  cdleme3b  40223  cdleme3c  40224  cdleme3e  40226  cdleme9b  40246  cdlemedb  40291  cdleme20zN  40295  cdleme19a  40297  cdlemf2  40556  tendoidcl  40763  dia1eldmN  41035  dialss  41040  dia1N  41047  diaglbN  41049  diaintclN  41052  docaclN  41118  doca2N  41120  djajN  41131  dibglbN  41160  dibintclN  41161  dihlsscpre  41228  dih2dimbALTN  41239  dih1  41280  dihglblem5apreN  41285  dihglblem5aN  41286  dihglblem2aN  41287  dihmeetcl  41339  dochvalr  41351  djhlj  41395