Theorem hllat 38538

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

Syntax hints:   → wi 4   ∈ wcel 2104  Latclat 18390  AtLatcal 38439  HLchlt 38525

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-dm 5687  df-iota 6496  df-fv 6552  df-ov 7416  df-atl 38473  df-cvlat 38497  df-hlat 38526

This theorem is referenced by:  hllatd  38539  hlpos  38541  hlatjcl  38542  hlatjcom  38543  hlatjidm  38544  hlatjass  38545  hlatj32  38547  hlatj4  38549  hlatlej1  38550  atnlej1  38555  atnlej2  38556  hlateq  38575  hlrelat5N  38577  hlrelat2  38579  cvr2N  38587  cvrval5  38591  cvrexchlem  38595  cvrexch  38596  cvratlem  38597  cvrat  38598  cvrat2  38605  atcvrj2b  38608  atltcvr  38611  atlelt  38614  cvrat3  38618  cvrat4  38619  cvrat42  38620  2atjm  38621  3noncolr2  38625  3dimlem3OLDN  38638  3dimlem4OLDN  38641  1cvrat  38652  ps-1  38653  ps-2  38654  hlatexch3N  38656  3at  38666  llnneat  38690  lplni2  38713  2atnelpln  38720  lplnneat  38721  lplnnelln  38722  islpln2a  38724  2lplnmN  38735  2llnmj  38736  2llnm2N  38744  2llnm3N  38745  2llnm4  38746  2llnmeqat  38747  islvol5  38755  3atnelvolN  38762  lvolneatN  38764  lvolnelln  38765  lvolnelpln  38766  2lplnm2N  38797  2lplnmj  38798  pmap11  38938  isline3  38952  lncvrelatN  38957  2atm2atN  38961  2llnma1b  38962  2llnma3r  38964  paddasslem16  39011  paddass  39014  padd12N  39015  pmod2iN  39025  pmodN  39026  pmapjat1  39029  pmapjat2  39030  pmapjlln1  39031  hlmod1i  39032  atmod2i1  39037  atmod2i2  39038  atmod3i1  39040  atmod3i2  39041  atmod4i1  39042  atmod4i2  39043  llnexch2N  39046  polsubN  39083  paddunN  39103  pmapj2N  39105  pmapocjN  39106  psubclinN  39124  paddatclN  39125  linepsubclN  39127  lhpocnle  39192  lhpjat2  39197  lhpmcvr  39199  lhpm0atN  39205  lhpmatb  39207  trlval2  39339  trlcl  39340  trlle  39360  cdlemd1  39374  cdleme0cp  39390  cdleme0cq  39391  cdleme1b  39402  cdleme1  39403  cdleme2  39404  cdleme3b  39405  cdleme3c  39406  cdleme3e  39408  cdleme9b  39428  cdlemedb  39473  cdleme20zN  39477  cdleme19a  39479  cdlemf2  39738  tendoidcl  39945  dia1eldmN  40217  dialss  40222  dia1N  40229  diaglbN  40231  diaintclN  40234  docaclN  40300  doca2N  40302  djajN  40313  dibglbN  40342  dibintclN  40343  dihlsscpre  40410  dih2dimbALTN  40421  dih1  40462  dihglblem5apreN  40467  dihglblem5aN  40468  dihglblem2aN  40469  dihmeetcl  40521  dochvalr  40533  djhlj  40577