Theorem hllat 39345

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

Syntax hints:   → wi 4   ∈ wcel 2106  Latclat 18489  AtLatcal 39246  HLchlt 39332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-dm 5699  df-iota 6516  df-fv 6571  df-ov 7434  df-atl 39280  df-cvlat 39304  df-hlat 39333

This theorem is referenced by:  hllatd  39346  hlpos  39348  hlatjcl  39349  hlatjcom  39350  hlatjidm  39351  hlatjass  39352  hlatj32  39354  hlatj4  39356  hlatlej1  39357  atnlej1  39362  atnlej2  39363  hlateq  39382  hlrelat5N  39384  hlrelat2  39386  cvr2N  39394  cvrval5  39398  cvrexchlem  39402  cvrexch  39403  cvratlem  39404  cvrat  39405  cvrat2  39412  atcvrj2b  39415  atltcvr  39418  atlelt  39421  cvrat3  39425  cvrat4  39426  cvrat42  39427  2atjm  39428  3noncolr2  39432  3dimlem3OLDN  39445  3dimlem4OLDN  39448  1cvrat  39459  ps-1  39460  ps-2  39461  hlatexch3N  39463  3at  39473  llnneat  39497  lplni2  39520  2atnelpln  39527  lplnneat  39528  lplnnelln  39529  islpln2a  39531  2lplnmN  39542  2llnmj  39543  2llnm2N  39551  2llnm3N  39552  2llnm4  39553  2llnmeqat  39554  islvol5  39562  3atnelvolN  39569  lvolneatN  39571  lvolnelln  39572  lvolnelpln  39573  2lplnm2N  39604  2lplnmj  39605  pmap11  39745  isline3  39759  lncvrelatN  39764  2atm2atN  39768  2llnma1b  39769  2llnma3r  39771  paddasslem16  39818  paddass  39821  padd12N  39822  pmod2iN  39832  pmodN  39833  pmapjat1  39836  pmapjat2  39837  pmapjlln1  39838  hlmod1i  39839  atmod2i1  39844  atmod2i2  39845  atmod3i1  39847  atmod3i2  39848  atmod4i1  39849  atmod4i2  39850  llnexch2N  39853  polsubN  39890  paddunN  39910  pmapj2N  39912  pmapocjN  39913  psubclinN  39931  paddatclN  39932  linepsubclN  39934  lhpocnle  39999  lhpjat2  40004  lhpmcvr  40006  lhpm0atN  40012  lhpmatb  40014  trlval2  40146  trlcl  40147  trlle  40167  cdlemd1  40181  cdleme0cp  40197  cdleme0cq  40198  cdleme1b  40209  cdleme1  40210  cdleme2  40211  cdleme3b  40212  cdleme3c  40213  cdleme3e  40215  cdleme9b  40235  cdlemedb  40280  cdleme20zN  40284  cdleme19a  40286  cdlemf2  40545  tendoidcl  40752  dia1eldmN  41024  dialss  41029  dia1N  41036  diaglbN  41038  diaintclN  41041  docaclN  41107  doca2N  41109  djajN  41120  dibglbN  41149  dibintclN  41150  dihlsscpre  41217  dih2dimbALTN  41228  dih1  41269  dihglblem5apreN  41274  dihglblem5aN  41275  dihglblem2aN  41276  dihmeetcl  41328  dochvalr  41340  djhlj  41384