Theorem hllat 40686

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Latclat 18655  AtLatcal 40587  HLchlt 40673

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-dm 5668  df-iota 6520  df-fv 6574  df-ov 7454  df-atl 40621  df-cvlat 40645  df-hlat 40674

This theorem is used by:  hllatd  40687  hlpos  40689  hlatjcl  40690  hlatjcom  40691  hlatjidm  40692  hlatjass  40693  hlatj32  40695  hlatj4  40697  hlatlej1  40698  atnlej1  40702  atnlej2  40703  hlateq  40722  hlrelat5N  40724  hlrelat2  40726  cvr2N  40734  cvrval5  40738  cvrexchlem  40742  cvrexch  40743  cvratlem  40744  cvrat  40745  cvrat2  40752  atcvrj2b  40755  atltcvr  40758  atlelt  40761  cvrat3  40765  cvrat4  40766  cvrat42  40767  2atjm  40768  3noncolr2  40772  3dimlem3OLDN  40785  3dimlem4OLDN  40788  1cvrat  40799  ps-1  40800  ps-2  40801  hlatexch3N  40803  3at  40813  llnneat  40837  lplni2  40860  2atnelpln  40867  lplnneat  40868  lplnnelln  40869  islpln2a  40871  2lplnmN  40882  2llnmj  40883  2llnm2N  40891  2llnm3N  40892  2llnm4  40893  2llnmeqat  40894  islvol5  40902  3atnelvolN  40909  lvolneatN  40911  lvolnelln  40912  lvolnelpln  40913  2lplnm2N  40944  2lplnmj  40945  pmap11  41085  isline3  41099  lncvrelatN  41104  2atm2atN  41108  2llnma1b  41109  2llnma3r  41111  paddasslem16  41158  paddass  41161  padd12N  41162  pmod2iN  41172  pmodN  41173  pmapjat1  41176  pmapjat2  41177  pmapjlln1  41178  hlmod1i  41179  atmod2i1  41184  atmod2i2  41185  atmod3i1  41187  atmod3i2  41188  atmod4i1  41189  atmod4i2  41190  llnexch2N  41193  polsubN  41230  paddunN  41250  pmapj2N  41252  pmapocjN  41253  psubclinN  41271  paddatclN  41272  linepsubclN  41274  lhpocnle  41339  lhpjat2  41344  lhpmcvr  41346  lhpm0atN  41352  lhpmatb  41354  trlval2  41486  trlcl  41487  trlle  41507  cdlemd1  41521  cdleme0cp  41537  cdleme0cq  41538  cdleme1b  41549  cdleme1  41550  cdleme2  41551  cdleme3b  41552  cdleme3c  41553  cdleme3e  41555  cdleme9b  41575  cdlemedb  41620  cdleme20zN  41624  cdleme19a  41626  cdlemf2  41885  tendoidcl  42092  dia1eldmN  42364  dialss  42369  dia1N  42376  diaglbN  42378  diaintclN  42381  docaclN  42447  doca2N  42449  djajN  42460  dibglbN  42489  dibintclN  42490  dihlsscpre  42557  dih2dimbALTN  42568  dih1  42609  dihglblem5apreN  42614  dihglblem5aN  42615  dihglblem2aN  42616  dihmeetcl  42668  dochvalr  42680  djhlj  42724