Theorem hllat 39364

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

Syntax hints:   → wi 4   ∈ wcel 2108  Latclat 18476  AtLatcal 39265  HLchlt 39351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-dm 5695  df-iota 6514  df-fv 6569  df-ov 7434  df-atl 39299  df-cvlat 39323  df-hlat 39352

This theorem is referenced by:  hllatd  39365  hlpos  39367  hlatjcl  39368  hlatjcom  39369  hlatjidm  39370  hlatjass  39371  hlatj32  39373  hlatj4  39375  hlatlej1  39376  atnlej1  39381  atnlej2  39382  hlateq  39401  hlrelat5N  39403  hlrelat2  39405  cvr2N  39413  cvrval5  39417  cvrexchlem  39421  cvrexch  39422  cvratlem  39423  cvrat  39424  cvrat2  39431  atcvrj2b  39434  atltcvr  39437  atlelt  39440  cvrat3  39444  cvrat4  39445  cvrat42  39446  2atjm  39447  3noncolr2  39451  3dimlem3OLDN  39464  3dimlem4OLDN  39467  1cvrat  39478  ps-1  39479  ps-2  39480  hlatexch3N  39482  3at  39492  llnneat  39516  lplni2  39539  2atnelpln  39546  lplnneat  39547  lplnnelln  39548  islpln2a  39550  2lplnmN  39561  2llnmj  39562  2llnm2N  39570  2llnm3N  39571  2llnm4  39572  2llnmeqat  39573  islvol5  39581  3atnelvolN  39588  lvolneatN  39590  lvolnelln  39591  lvolnelpln  39592  2lplnm2N  39623  2lplnmj  39624  pmap11  39764  isline3  39778  lncvrelatN  39783  2atm2atN  39787  2llnma1b  39788  2llnma3r  39790  paddasslem16  39837  paddass  39840  padd12N  39841  pmod2iN  39851  pmodN  39852  pmapjat1  39855  pmapjat2  39856  pmapjlln1  39857  hlmod1i  39858  atmod2i1  39863  atmod2i2  39864  atmod3i1  39866  atmod3i2  39867  atmod4i1  39868  atmod4i2  39869  llnexch2N  39872  polsubN  39909  paddunN  39929  pmapj2N  39931  pmapocjN  39932  psubclinN  39950  paddatclN  39951  linepsubclN  39953  lhpocnle  40018  lhpjat2  40023  lhpmcvr  40025  lhpm0atN  40031  lhpmatb  40033  trlval2  40165  trlcl  40166  trlle  40186  cdlemd1  40200  cdleme0cp  40216  cdleme0cq  40217  cdleme1b  40228  cdleme1  40229  cdleme2  40230  cdleme3b  40231  cdleme3c  40232  cdleme3e  40234  cdleme9b  40254  cdlemedb  40299  cdleme20zN  40303  cdleme19a  40305  cdlemf2  40564  tendoidcl  40771  dia1eldmN  41043  dialss  41048  dia1N  41055  diaglbN  41057  diaintclN  41060  docaclN  41126  doca2N  41128  djajN  41139  dibglbN  41168  dibintclN  41169  dihlsscpre  41236  dih2dimbALTN  41247  dih1  41288  dihglblem5apreN  41293  dihglblem5aN  41294  dihglblem2aN  41295  dihmeetcl  41347  dochvalr  41359  djhlj  41403