Theorem hllat 35977

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

Syntax hints:   → wi 4   ∈ wcel 2051  Latclat 17526  AtLatcal 35878  HLchlt 35964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-ral 3088  df-rex 3089  df-rab 3092  df-v 3412  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-br 4927  df-dm 5414  df-iota 6150  df-fv 6194  df-ov 6978  df-atl 35912  df-cvlat 35936  df-hlat 35965

This theorem is referenced by:  hllatd  35978  hlpos  35980  hlatjcl  35981  hlatjcom  35982  hlatjidm  35983  hlatjass  35984  hlatj32  35986  hlatj4  35988  hlatlej1  35989  atnlej1  35993  atnlej2  35994  hlateq  36013  hlrelat5N  36015  hlrelat2  36017  cvr2N  36025  cvrval5  36029  cvrexchlem  36033  cvrexch  36034  cvratlem  36035  cvrat  36036  cvrat2  36043  atcvrj2b  36046  atltcvr  36049  atlelt  36052  cvrat3  36056  cvrat4  36057  cvrat42  36058  2atjm  36059  3noncolr2  36063  3dimlem3OLDN  36076  3dimlem4OLDN  36079  1cvrat  36090  ps-1  36091  ps-2  36092  hlatexch3N  36094  3at  36104  llnneat  36128  lplni2  36151  2atnelpln  36158  lplnneat  36159  lplnnelln  36160  islpln2a  36162  2lplnmN  36173  2llnmj  36174  2llnm2N  36182  2llnm3N  36183  2llnm4  36184  2llnmeqat  36185  islvol5  36193  3atnelvolN  36200  lvolneatN  36202  lvolnelln  36203  lvolnelpln  36204  2lplnm2N  36235  2lplnmj  36236  pmap11  36376  isline3  36390  lncvrelatN  36395  2atm2atN  36399  2llnma1b  36400  2llnma3r  36402  paddasslem16  36449  paddass  36452  padd12N  36453  pmod2iN  36463  pmodN  36464  pmapjat1  36467  pmapjat2  36468  pmapjlln1  36469  hlmod1i  36470  atmod2i1  36475  atmod2i2  36476  atmod3i1  36478  atmod3i2  36479  atmod4i1  36480  atmod4i2  36481  llnexch2N  36484  polsubN  36521  paddunN  36541  pmapj2N  36543  pmapocjN  36544  psubclinN  36562  paddatclN  36563  linepsubclN  36565  lhpocnle  36630  lhpjat2  36635  lhpmcvr  36637  lhpm0atN  36643  lhpmatb  36645  trlval2  36777  trlcl  36778  trlle  36798  cdlemd1  36812  cdleme0cp  36828  cdleme0cq  36829  cdleme1b  36840  cdleme1  36841  cdleme2  36842  cdleme3b  36843  cdleme3c  36844  cdleme3e  36846  cdleme9b  36866  cdlemedb  36911  cdleme20zN  36915  cdleme19a  36917  cdlemf2  37176  tendoidcl  37383  dia1eldmN  37655  dialss  37660  dia1N  37667  diaglbN  37669  diaintclN  37672  docaclN  37738  doca2N  37740  djajN  37751  dibglbN  37780  dibintclN  37781  dihlsscpre  37848  dih2dimbALTN  37859  dih1  37900  dihglblem5apreN  37905  dihglblem5aN  37906  dihglblem2aN  37907  dihmeetcl  37959  dochvalr  37971  djhlj  38015