Theorem hllat 39736

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

Syntax hints:   → wi 4   ∈ wcel 2114  Latclat 18366  AtLatcal 39637  HLchlt 39723

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-dm 5642  df-iota 6456  df-fv 6508  df-ov 7371  df-atl 39671  df-cvlat 39695  df-hlat 39724

This theorem is referenced by:  hllatd  39737  hlpos  39739  hlatjcl  39740  hlatjcom  39741  hlatjidm  39742  hlatjass  39743  hlatj32  39745  hlatj4  39747  hlatlej1  39748  atnlej1  39752  atnlej2  39753  hlateq  39772  hlrelat5N  39774  hlrelat2  39776  cvr2N  39784  cvrval5  39788  cvrexchlem  39792  cvrexch  39793  cvratlem  39794  cvrat  39795  cvrat2  39802  atcvrj2b  39805  atltcvr  39808  atlelt  39811  cvrat3  39815  cvrat4  39816  cvrat42  39817  2atjm  39818  3noncolr2  39822  3dimlem3OLDN  39835  3dimlem4OLDN  39838  1cvrat  39849  ps-1  39850  ps-2  39851  hlatexch3N  39853  3at  39863  llnneat  39887  lplni2  39910  2atnelpln  39917  lplnneat  39918  lplnnelln  39919  islpln2a  39921  2lplnmN  39932  2llnmj  39933  2llnm2N  39941  2llnm3N  39942  2llnm4  39943  2llnmeqat  39944  islvol5  39952  3atnelvolN  39959  lvolneatN  39961  lvolnelln  39962  lvolnelpln  39963  2lplnm2N  39994  2lplnmj  39995  pmap11  40135  isline3  40149  lncvrelatN  40154  2atm2atN  40158  2llnma1b  40159  2llnma3r  40161  paddasslem16  40208  paddass  40211  padd12N  40212  pmod2iN  40222  pmodN  40223  pmapjat1  40226  pmapjat2  40227  pmapjlln1  40228  hlmod1i  40229  atmod2i1  40234  atmod2i2  40235  atmod3i1  40237  atmod3i2  40238  atmod4i1  40239  atmod4i2  40240  llnexch2N  40243  polsubN  40280  paddunN  40300  pmapj2N  40302  pmapocjN  40303  psubclinN  40321  paddatclN  40322  linepsubclN  40324  lhpocnle  40389  lhpjat2  40394  lhpmcvr  40396  lhpm0atN  40402  lhpmatb  40404  trlval2  40536  trlcl  40537  trlle  40557  cdlemd1  40571  cdleme0cp  40587  cdleme0cq  40588  cdleme1b  40599  cdleme1  40600  cdleme2  40601  cdleme3b  40602  cdleme3c  40603  cdleme3e  40605  cdleme9b  40625  cdlemedb  40670  cdleme20zN  40674  cdleme19a  40676  cdlemf2  40935  tendoidcl  41142  dia1eldmN  41414  dialss  41419  dia1N  41426  diaglbN  41428  diaintclN  41431  docaclN  41497  doca2N  41499  djajN  41510  dibglbN  41539  dibintclN  41540  dihlsscpre  41607  dih2dimbALTN  41618  dih1  41659  dihglblem5apreN  41664  dihglblem5aN  41665  dihglblem2aN  41666  dihmeetcl  41718  dochvalr  41730  djhlj  41774