Theorem hllat 40118

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

Syntax hints:   → wi 4   ∈ wcel 2143  Latclat 18488  AtLatcal 40019  HLchlt 40105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-dm 5673  df-iota 6494  df-fv 6546  df-ov 7415  df-atl 40053  df-cvlat 40077  df-hlat 40106

This theorem is referenced by:  hllatd  40119  hlpos  40121  hlatjcl  40122  hlatjcom  40123  hlatjidm  40124  hlatjass  40125  hlatj32  40127  hlatj4  40129  hlatlej1  40130  atnlej1  40134  atnlej2  40135  hlateq  40154  hlrelat5N  40156  hlrelat2  40158  cvr2N  40166  cvrval5  40170  cvrexchlem  40174  cvrexch  40175  cvratlem  40176  cvrat  40177  cvrat2  40184  atcvrj2b  40187  atltcvr  40190  atlelt  40193  cvrat3  40197  cvrat4  40198  cvrat42  40199  2atjm  40200  3noncolr2  40204  3dimlem3OLDN  40217  3dimlem4OLDN  40220  1cvrat  40231  ps-1  40232  ps-2  40233  hlatexch3N  40235  3at  40245  llnneat  40269  lplni2  40292  2atnelpln  40299  lplnneat  40300  lplnnelln  40301  islpln2a  40303  2lplnmN  40314  2llnmj  40315  2llnm2N  40323  2llnm3N  40324  2llnm4  40325  2llnmeqat  40326  islvol5  40334  3atnelvolN  40341  lvolneatN  40343  lvolnelln  40344  lvolnelpln  40345  2lplnm2N  40376  2lplnmj  40377  pmap11  40517  isline3  40531  lncvrelatN  40536  2atm2atN  40540  2llnma1b  40541  2llnma3r  40543  paddasslem16  40590  paddass  40593  padd12N  40594  pmod2iN  40604  pmodN  40605  pmapjat1  40608  pmapjat2  40609  pmapjlln1  40610  hlmod1i  40611  atmod2i1  40616  atmod2i2  40617  atmod3i1  40619  atmod3i2  40620  atmod4i1  40621  atmod4i2  40622  llnexch2N  40625  polsubN  40662  paddunN  40682  pmapj2N  40684  pmapocjN  40685  psubclinN  40703  paddatclN  40704  linepsubclN  40706  lhpocnle  40771  lhpjat2  40776  lhpmcvr  40778  lhpm0atN  40784  lhpmatb  40786  trlval2  40918  trlcl  40919  trlle  40939  cdlemd1  40953  cdleme0cp  40969  cdleme0cq  40970  cdleme1b  40981  cdleme1  40982  cdleme2  40983  cdleme3b  40984  cdleme3c  40985  cdleme3e  40987  cdleme9b  41007  cdlemedb  41052  cdleme20zN  41056  cdleme19a  41058  cdlemf2  41317  tendoidcl  41524  dia1eldmN  41796  dialss  41801  dia1N  41808  diaglbN  41810  diaintclN  41813  docaclN  41879  doca2N  41881  djajN  41892  dibglbN  41921  dibintclN  41922  dihlsscpre  41989  dih2dimbALTN  42000  dih1  42041  dihglblem5apreN  42046  dihglblem5aN  42047  dihglblem2aN  42048  dihmeetcl  42100  dochvalr  42112  djhlj  42156