Theorem hllat 39823

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

Syntax hints:   → wi 4   ∈ wcel 2114  Latclat 18388  AtLatcal 39724  HLchlt 39810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-dm 5634  df-iota 6448  df-fv 6500  df-ov 7363  df-atl 39758  df-cvlat 39782  df-hlat 39811

This theorem is referenced by:  hllatd  39824  hlpos  39826  hlatjcl  39827  hlatjcom  39828  hlatjidm  39829  hlatjass  39830  hlatj32  39832  hlatj4  39834  hlatlej1  39835  atnlej1  39839  atnlej2  39840  hlateq  39859  hlrelat5N  39861  hlrelat2  39863  cvr2N  39871  cvrval5  39875  cvrexchlem  39879  cvrexch  39880  cvratlem  39881  cvrat  39882  cvrat2  39889  atcvrj2b  39892  atltcvr  39895  atlelt  39898  cvrat3  39902  cvrat4  39903  cvrat42  39904  2atjm  39905  3noncolr2  39909  3dimlem3OLDN  39922  3dimlem4OLDN  39925  1cvrat  39936  ps-1  39937  ps-2  39938  hlatexch3N  39940  3at  39950  llnneat  39974  lplni2  39997  2atnelpln  40004  lplnneat  40005  lplnnelln  40006  islpln2a  40008  2lplnmN  40019  2llnmj  40020  2llnm2N  40028  2llnm3N  40029  2llnm4  40030  2llnmeqat  40031  islvol5  40039  3atnelvolN  40046  lvolneatN  40048  lvolnelln  40049  lvolnelpln  40050  2lplnm2N  40081  2lplnmj  40082  pmap11  40222  isline3  40236  lncvrelatN  40241  2atm2atN  40245  2llnma1b  40246  2llnma3r  40248  paddasslem16  40295  paddass  40298  padd12N  40299  pmod2iN  40309  pmodN  40310  pmapjat1  40313  pmapjat2  40314  pmapjlln1  40315  hlmod1i  40316  atmod2i1  40321  atmod2i2  40322  atmod3i1  40324  atmod3i2  40325  atmod4i1  40326  atmod4i2  40327  llnexch2N  40330  polsubN  40367  paddunN  40387  pmapj2N  40389  pmapocjN  40390  psubclinN  40408  paddatclN  40409  linepsubclN  40411  lhpocnle  40476  lhpjat2  40481  lhpmcvr  40483  lhpm0atN  40489  lhpmatb  40491  trlval2  40623  trlcl  40624  trlle  40644  cdlemd1  40658  cdleme0cp  40674  cdleme0cq  40675  cdleme1b  40686  cdleme1  40687  cdleme2  40688  cdleme3b  40689  cdleme3c  40690  cdleme3e  40692  cdleme9b  40712  cdlemedb  40757  cdleme20zN  40761  cdleme19a  40763  cdlemf2  41022  tendoidcl  41229  dia1eldmN  41501  dialss  41506  dia1N  41513  diaglbN  41515  diaintclN  41518  docaclN  41584  doca2N  41586  djajN  41597  dibglbN  41626  dibintclN  41627  dihlsscpre  41694  dih2dimbALTN  41705  dih1  41746  dihglblem5apreN  41751  dihglblem5aN  41752  dihglblem2aN  41753  dihmeetcl  41805  dochvalr  41817  djhlj  41861