Theorem hllat 39402

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

Syntax hints:   → wi 4   ∈ wcel 2111  Latclat 18332  AtLatcal 39303  HLchlt 39389

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-dm 5621  df-iota 6432  df-fv 6484  df-ov 7344  df-atl 39337  df-cvlat 39361  df-hlat 39390

This theorem is referenced by:  hllatd  39403  hlpos  39405  hlatjcl  39406  hlatjcom  39407  hlatjidm  39408  hlatjass  39409  hlatj32  39411  hlatj4  39413  hlatlej1  39414  atnlej1  39418  atnlej2  39419  hlateq  39438  hlrelat5N  39440  hlrelat2  39442  cvr2N  39450  cvrval5  39454  cvrexchlem  39458  cvrexch  39459  cvratlem  39460  cvrat  39461  cvrat2  39468  atcvrj2b  39471  atltcvr  39474  atlelt  39477  cvrat3  39481  cvrat4  39482  cvrat42  39483  2atjm  39484  3noncolr2  39488  3dimlem3OLDN  39501  3dimlem4OLDN  39504  1cvrat  39515  ps-1  39516  ps-2  39517  hlatexch3N  39519  3at  39529  llnneat  39553  lplni2  39576  2atnelpln  39583  lplnneat  39584  lplnnelln  39585  islpln2a  39587  2lplnmN  39598  2llnmj  39599  2llnm2N  39607  2llnm3N  39608  2llnm4  39609  2llnmeqat  39610  islvol5  39618  3atnelvolN  39625  lvolneatN  39627  lvolnelln  39628  lvolnelpln  39629  2lplnm2N  39660  2lplnmj  39661  pmap11  39801  isline3  39815  lncvrelatN  39820  2atm2atN  39824  2llnma1b  39825  2llnma3r  39827  paddasslem16  39874  paddass  39877  padd12N  39878  pmod2iN  39888  pmodN  39889  pmapjat1  39892  pmapjat2  39893  pmapjlln1  39894  hlmod1i  39895  atmod2i1  39900  atmod2i2  39901  atmod3i1  39903  atmod3i2  39904  atmod4i1  39905  atmod4i2  39906  llnexch2N  39909  polsubN  39946  paddunN  39966  pmapj2N  39968  pmapocjN  39969  psubclinN  39987  paddatclN  39988  linepsubclN  39990  lhpocnle  40055  lhpjat2  40060  lhpmcvr  40062  lhpm0atN  40068  lhpmatb  40070  trlval2  40202  trlcl  40203  trlle  40223  cdlemd1  40237  cdleme0cp  40253  cdleme0cq  40254  cdleme1b  40265  cdleme1  40266  cdleme2  40267  cdleme3b  40268  cdleme3c  40269  cdleme3e  40271  cdleme9b  40291  cdlemedb  40336  cdleme20zN  40340  cdleme19a  40342  cdlemf2  40601  tendoidcl  40808  dia1eldmN  41080  dialss  41085  dia1N  41092  diaglbN  41094  diaintclN  41097  docaclN  41163  doca2N  41165  djajN  41176  dibglbN  41205  dibintclN  41206  dihlsscpre  41273  dih2dimbALTN  41284  dih1  41325  dihglblem5apreN  41330  dihglblem5aN  41331  dihglblem2aN  41332  dihmeetcl  41384  dochvalr  41396  djhlj  41440