Theorem hllat 39855

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

Syntax hints:   → wi 4   ∈ wcel 2119  Latclat 18388  AtLatcal 39756  HLchlt 39842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-dm 5628  df-iota 6441  df-fv 6493  df-ov 7359  df-atl 39790  df-cvlat 39814  df-hlat 39843

This theorem is referenced by:  hllatd  39856  hlpos  39858  hlatjcl  39859  hlatjcom  39860  hlatjidm  39861  hlatjass  39862  hlatj32  39864  hlatj4  39866  hlatlej1  39867  atnlej1  39871  atnlej2  39872  hlateq  39891  hlrelat5N  39893  hlrelat2  39895  cvr2N  39903  cvrval5  39907  cvrexchlem  39911  cvrexch  39912  cvratlem  39913  cvrat  39914  cvrat2  39921  atcvrj2b  39924  atltcvr  39927  atlelt  39930  cvrat3  39934  cvrat4  39935  cvrat42  39936  2atjm  39937  3noncolr2  39941  3dimlem3OLDN  39954  3dimlem4OLDN  39957  1cvrat  39968  ps-1  39969  ps-2  39970  hlatexch3N  39972  3at  39982  llnneat  40006  lplni2  40029  2atnelpln  40036  lplnneat  40037  lplnnelln  40038  islpln2a  40040  2lplnmN  40051  2llnmj  40052  2llnm2N  40060  2llnm3N  40061  2llnm4  40062  2llnmeqat  40063  islvol5  40071  3atnelvolN  40078  lvolneatN  40080  lvolnelln  40081  lvolnelpln  40082  2lplnm2N  40113  2lplnmj  40114  pmap11  40254  isline3  40268  lncvrelatN  40273  2atm2atN  40277  2llnma1b  40278  2llnma3r  40280  paddasslem16  40327  paddass  40330  padd12N  40331  pmod2iN  40341  pmodN  40342  pmapjat1  40345  pmapjat2  40346  pmapjlln1  40347  hlmod1i  40348  atmod2i1  40353  atmod2i2  40354  atmod3i1  40356  atmod3i2  40357  atmod4i1  40358  atmod4i2  40359  llnexch2N  40362  polsubN  40399  paddunN  40419  pmapj2N  40421  pmapocjN  40422  psubclinN  40440  paddatclN  40441  linepsubclN  40443  lhpocnle  40508  lhpjat2  40513  lhpmcvr  40515  lhpm0atN  40521  lhpmatb  40523  trlval2  40655  trlcl  40656  trlle  40676  cdlemd1  40690  cdleme0cp  40706  cdleme0cq  40707  cdleme1b  40718  cdleme1  40719  cdleme2  40720  cdleme3b  40721  cdleme3c  40722  cdleme3e  40724  cdleme9b  40744  cdlemedb  40789  cdleme20zN  40793  cdleme19a  40795  cdlemf2  41054  tendoidcl  41261  dia1eldmN  41533  dialss  41538  dia1N  41545  diaglbN  41547  diaintclN  41550  docaclN  41616  doca2N  41618  djajN  41629  dibglbN  41658  dibintclN  41659  dihlsscpre  41726  dih2dimbALTN  41737  dih1  41778  dihglblem5apreN  41783  dihglblem5aN  41784  dihglblem2aN  41785  dihmeetcl  41837  dochvalr  41849  djhlj  41893