Theorem hllat 37377

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

Syntax hints:   → wi 4   ∈ wcel 2106  Latclat 18149  AtLatcal 37278  HLchlt 37364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-dm 5599  df-iota 6391  df-fv 6441  df-ov 7278  df-atl 37312  df-cvlat 37336  df-hlat 37365

This theorem is referenced by:  hllatd  37378  hlpos  37380  hlatjcl  37381  hlatjcom  37382  hlatjidm  37383  hlatjass  37384  hlatj32  37386  hlatj4  37388  hlatlej1  37389  atnlej1  37393  atnlej2  37394  hlateq  37413  hlrelat5N  37415  hlrelat2  37417  cvr2N  37425  cvrval5  37429  cvrexchlem  37433  cvrexch  37434  cvratlem  37435  cvrat  37436  cvrat2  37443  atcvrj2b  37446  atltcvr  37449  atlelt  37452  cvrat3  37456  cvrat4  37457  cvrat42  37458  2atjm  37459  3noncolr2  37463  3dimlem3OLDN  37476  3dimlem4OLDN  37479  1cvrat  37490  ps-1  37491  ps-2  37492  hlatexch3N  37494  3at  37504  llnneat  37528  lplni2  37551  2atnelpln  37558  lplnneat  37559  lplnnelln  37560  islpln2a  37562  2lplnmN  37573  2llnmj  37574  2llnm2N  37582  2llnm3N  37583  2llnm4  37584  2llnmeqat  37585  islvol5  37593  3atnelvolN  37600  lvolneatN  37602  lvolnelln  37603  lvolnelpln  37604  2lplnm2N  37635  2lplnmj  37636  pmap11  37776  isline3  37790  lncvrelatN  37795  2atm2atN  37799  2llnma1b  37800  2llnma3r  37802  paddasslem16  37849  paddass  37852  padd12N  37853  pmod2iN  37863  pmodN  37864  pmapjat1  37867  pmapjat2  37868  pmapjlln1  37869  hlmod1i  37870  atmod2i1  37875  atmod2i2  37876  atmod3i1  37878  atmod3i2  37879  atmod4i1  37880  atmod4i2  37881  llnexch2N  37884  polsubN  37921  paddunN  37941  pmapj2N  37943  pmapocjN  37944  psubclinN  37962  paddatclN  37963  linepsubclN  37965  lhpocnle  38030  lhpjat2  38035  lhpmcvr  38037  lhpm0atN  38043  lhpmatb  38045  trlval2  38177  trlcl  38178  trlle  38198  cdlemd1  38212  cdleme0cp  38228  cdleme0cq  38229  cdleme1b  38240  cdleme1  38241  cdleme2  38242  cdleme3b  38243  cdleme3c  38244  cdleme3e  38246  cdleme9b  38266  cdlemedb  38311  cdleme20zN  38315  cdleme19a  38317  cdlemf2  38576  tendoidcl  38783  dia1eldmN  39055  dialss  39060  dia1N  39067  diaglbN  39069  diaintclN  39072  docaclN  39138  doca2N  39140  djajN  39151  dibglbN  39180  dibintclN  39181  dihlsscpre  39248  dih2dimbALTN  39259  dih1  39300  dihglblem5apreN  39305  dihglblem5aN  39306  dihglblem2aN  39307  dihmeetcl  39359  dochvalr  39371  djhlj  39415