Theorem hllat 38221

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

Syntax hints:   → wi 4   ∈ wcel 2106  Latclat 18380  AtLatcal 38122  HLchlt 38208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-dm 5685  df-iota 6492  df-fv 6548  df-ov 7408  df-atl 38156  df-cvlat 38180  df-hlat 38209

This theorem is referenced by:  hllatd  38222  hlpos  38224  hlatjcl  38225  hlatjcom  38226  hlatjidm  38227  hlatjass  38228  hlatj32  38230  hlatj4  38232  hlatlej1  38233  atnlej1  38238  atnlej2  38239  hlateq  38258  hlrelat5N  38260  hlrelat2  38262  cvr2N  38270  cvrval5  38274  cvrexchlem  38278  cvrexch  38279  cvratlem  38280  cvrat  38281  cvrat2  38288  atcvrj2b  38291  atltcvr  38294  atlelt  38297  cvrat3  38301  cvrat4  38302  cvrat42  38303  2atjm  38304  3noncolr2  38308  3dimlem3OLDN  38321  3dimlem4OLDN  38324  1cvrat  38335  ps-1  38336  ps-2  38337  hlatexch3N  38339  3at  38349  llnneat  38373  lplni2  38396  2atnelpln  38403  lplnneat  38404  lplnnelln  38405  islpln2a  38407  2lplnmN  38418  2llnmj  38419  2llnm2N  38427  2llnm3N  38428  2llnm4  38429  2llnmeqat  38430  islvol5  38438  3atnelvolN  38445  lvolneatN  38447  lvolnelln  38448  lvolnelpln  38449  2lplnm2N  38480  2lplnmj  38481  pmap11  38621  isline3  38635  lncvrelatN  38640  2atm2atN  38644  2llnma1b  38645  2llnma3r  38647  paddasslem16  38694  paddass  38697  padd12N  38698  pmod2iN  38708  pmodN  38709  pmapjat1  38712  pmapjat2  38713  pmapjlln1  38714  hlmod1i  38715  atmod2i1  38720  atmod2i2  38721  atmod3i1  38723  atmod3i2  38724  atmod4i1  38725  atmod4i2  38726  llnexch2N  38729  polsubN  38766  paddunN  38786  pmapj2N  38788  pmapocjN  38789  psubclinN  38807  paddatclN  38808  linepsubclN  38810  lhpocnle  38875  lhpjat2  38880  lhpmcvr  38882  lhpm0atN  38888  lhpmatb  38890  trlval2  39022  trlcl  39023  trlle  39043  cdlemd1  39057  cdleme0cp  39073  cdleme0cq  39074  cdleme1b  39085  cdleme1  39086  cdleme2  39087  cdleme3b  39088  cdleme3c  39089  cdleme3e  39091  cdleme9b  39111  cdlemedb  39156  cdleme20zN  39160  cdleme19a  39162  cdlemf2  39421  tendoidcl  39628  dia1eldmN  39900  dialss  39905  dia1N  39912  diaglbN  39914  diaintclN  39917  docaclN  39983  doca2N  39985  djajN  39996  dibglbN  40025  dibintclN  40026  dihlsscpre  40093  dih2dimbALTN  40104  dih1  40145  dihglblem5apreN  40150  dihglblem5aN  40151  dihglblem2aN  40152  dihmeetcl  40204  dochvalr  40216  djhlj  40260