Theorem hllat 39381

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

Syntax hints:   → wi 4   ∈ wcel 2108  Latclat 18441  AtLatcal 39282  HLchlt 39368

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-dm 5664  df-iota 6484  df-fv 6539  df-ov 7408  df-atl 39316  df-cvlat 39340  df-hlat 39369

This theorem is referenced by:  hllatd  39382  hlpos  39384  hlatjcl  39385  hlatjcom  39386  hlatjidm  39387  hlatjass  39388  hlatj32  39390  hlatj4  39392  hlatlej1  39393  atnlej1  39398  atnlej2  39399  hlateq  39418  hlrelat5N  39420  hlrelat2  39422  cvr2N  39430  cvrval5  39434  cvrexchlem  39438  cvrexch  39439  cvratlem  39440  cvrat  39441  cvrat2  39448  atcvrj2b  39451  atltcvr  39454  atlelt  39457  cvrat3  39461  cvrat4  39462  cvrat42  39463  2atjm  39464  3noncolr2  39468  3dimlem3OLDN  39481  3dimlem4OLDN  39484  1cvrat  39495  ps-1  39496  ps-2  39497  hlatexch3N  39499  3at  39509  llnneat  39533  lplni2  39556  2atnelpln  39563  lplnneat  39564  lplnnelln  39565  islpln2a  39567  2lplnmN  39578  2llnmj  39579  2llnm2N  39587  2llnm3N  39588  2llnm4  39589  2llnmeqat  39590  islvol5  39598  3atnelvolN  39605  lvolneatN  39607  lvolnelln  39608  lvolnelpln  39609  2lplnm2N  39640  2lplnmj  39641  pmap11  39781  isline3  39795  lncvrelatN  39800  2atm2atN  39804  2llnma1b  39805  2llnma3r  39807  paddasslem16  39854  paddass  39857  padd12N  39858  pmod2iN  39868  pmodN  39869  pmapjat1  39872  pmapjat2  39873  pmapjlln1  39874  hlmod1i  39875  atmod2i1  39880  atmod2i2  39881  atmod3i1  39883  atmod3i2  39884  atmod4i1  39885  atmod4i2  39886  llnexch2N  39889  polsubN  39926  paddunN  39946  pmapj2N  39948  pmapocjN  39949  psubclinN  39967  paddatclN  39968  linepsubclN  39970  lhpocnle  40035  lhpjat2  40040  lhpmcvr  40042  lhpm0atN  40048  lhpmatb  40050  trlval2  40182  trlcl  40183  trlle  40203  cdlemd1  40217  cdleme0cp  40233  cdleme0cq  40234  cdleme1b  40245  cdleme1  40246  cdleme2  40247  cdleme3b  40248  cdleme3c  40249  cdleme3e  40251  cdleme9b  40271  cdlemedb  40316  cdleme20zN  40320  cdleme19a  40322  cdlemf2  40581  tendoidcl  40788  dia1eldmN  41060  dialss  41065  dia1N  41072  diaglbN  41074  diaintclN  41077  docaclN  41143  doca2N  41145  djajN  41156  dibglbN  41185  dibintclN  41186  dihlsscpre  41253  dih2dimbALTN  41264  dih1  41305  dihglblem5apreN  41310  dihglblem5aN  41311  dihglblem2aN  41312  dihmeetcl  41364  dochvalr  41376  djhlj  41420