Theorem hllat 39623

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

Syntax hints:   → wi 4   ∈ wcel 2113  Latclat 18354  AtLatcal 39524  HLchlt 39610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-dm 5634  df-iota 6448  df-fv 6500  df-ov 7361  df-atl 39558  df-cvlat 39582  df-hlat 39611

This theorem is referenced by:  hllatd  39624  hlpos  39626  hlatjcl  39627  hlatjcom  39628  hlatjidm  39629  hlatjass  39630  hlatj32  39632  hlatj4  39634  hlatlej1  39635  atnlej1  39639  atnlej2  39640  hlateq  39659  hlrelat5N  39661  hlrelat2  39663  cvr2N  39671  cvrval5  39675  cvrexchlem  39679  cvrexch  39680  cvratlem  39681  cvrat  39682  cvrat2  39689  atcvrj2b  39692  atltcvr  39695  atlelt  39698  cvrat3  39702  cvrat4  39703  cvrat42  39704  2atjm  39705  3noncolr2  39709  3dimlem3OLDN  39722  3dimlem4OLDN  39725  1cvrat  39736  ps-1  39737  ps-2  39738  hlatexch3N  39740  3at  39750  llnneat  39774  lplni2  39797  2atnelpln  39804  lplnneat  39805  lplnnelln  39806  islpln2a  39808  2lplnmN  39819  2llnmj  39820  2llnm2N  39828  2llnm3N  39829  2llnm4  39830  2llnmeqat  39831  islvol5  39839  3atnelvolN  39846  lvolneatN  39848  lvolnelln  39849  lvolnelpln  39850  2lplnm2N  39881  2lplnmj  39882  pmap11  40022  isline3  40036  lncvrelatN  40041  2atm2atN  40045  2llnma1b  40046  2llnma3r  40048  paddasslem16  40095  paddass  40098  padd12N  40099  pmod2iN  40109  pmodN  40110  pmapjat1  40113  pmapjat2  40114  pmapjlln1  40115  hlmod1i  40116  atmod2i1  40121  atmod2i2  40122  atmod3i1  40124  atmod3i2  40125  atmod4i1  40126  atmod4i2  40127  llnexch2N  40130  polsubN  40167  paddunN  40187  pmapj2N  40189  pmapocjN  40190  psubclinN  40208  paddatclN  40209  linepsubclN  40211  lhpocnle  40276  lhpjat2  40281  lhpmcvr  40283  lhpm0atN  40289  lhpmatb  40291  trlval2  40423  trlcl  40424  trlle  40444  cdlemd1  40458  cdleme0cp  40474  cdleme0cq  40475  cdleme1b  40486  cdleme1  40487  cdleme2  40488  cdleme3b  40489  cdleme3c  40490  cdleme3e  40492  cdleme9b  40512  cdlemedb  40557  cdleme20zN  40561  cdleme19a  40563  cdlemf2  40822  tendoidcl  41029  dia1eldmN  41301  dialss  41306  dia1N  41313  diaglbN  41315  diaintclN  41318  docaclN  41384  doca2N  41386  djajN  41397  dibglbN  41426  dibintclN  41427  dihlsscpre  41494  dih2dimbALTN  41505  dih1  41546  dihglblem5apreN  41551  dihglblem5aN  41552  dihglblem2aN  41553  dihmeetcl  41605  dochvalr  41617  djhlj  41661