Theorem hllat 38727

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

Syntax hints:   → wi 4   ∈ wcel 2098  Latclat 18388  AtLatcal 38628  HLchlt 38714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-dm 5677  df-iota 6486  df-fv 6542  df-ov 7405  df-atl 38662  df-cvlat 38686  df-hlat 38715

This theorem is referenced by:  hllatd  38728  hlpos  38730  hlatjcl  38731  hlatjcom  38732  hlatjidm  38733  hlatjass  38734  hlatj32  38736  hlatj4  38738  hlatlej1  38739  atnlej1  38744  atnlej2  38745  hlateq  38764  hlrelat5N  38766  hlrelat2  38768  cvr2N  38776  cvrval5  38780  cvrexchlem  38784  cvrexch  38785  cvratlem  38786  cvrat  38787  cvrat2  38794  atcvrj2b  38797  atltcvr  38800  atlelt  38803  cvrat3  38807  cvrat4  38808  cvrat42  38809  2atjm  38810  3noncolr2  38814  3dimlem3OLDN  38827  3dimlem4OLDN  38830  1cvrat  38841  ps-1  38842  ps-2  38843  hlatexch3N  38845  3at  38855  llnneat  38879  lplni2  38902  2atnelpln  38909  lplnneat  38910  lplnnelln  38911  islpln2a  38913  2lplnmN  38924  2llnmj  38925  2llnm2N  38933  2llnm3N  38934  2llnm4  38935  2llnmeqat  38936  islvol5  38944  3atnelvolN  38951  lvolneatN  38953  lvolnelln  38954  lvolnelpln  38955  2lplnm2N  38986  2lplnmj  38987  pmap11  39127  isline3  39141  lncvrelatN  39146  2atm2atN  39150  2llnma1b  39151  2llnma3r  39153  paddasslem16  39200  paddass  39203  padd12N  39204  pmod2iN  39214  pmodN  39215  pmapjat1  39218  pmapjat2  39219  pmapjlln1  39220  hlmod1i  39221  atmod2i1  39226  atmod2i2  39227  atmod3i1  39229  atmod3i2  39230  atmod4i1  39231  atmod4i2  39232  llnexch2N  39235  polsubN  39272  paddunN  39292  pmapj2N  39294  pmapocjN  39295  psubclinN  39313  paddatclN  39314  linepsubclN  39316  lhpocnle  39381  lhpjat2  39386  lhpmcvr  39388  lhpm0atN  39394  lhpmatb  39396  trlval2  39528  trlcl  39529  trlle  39549  cdlemd1  39563  cdleme0cp  39579  cdleme0cq  39580  cdleme1b  39591  cdleme1  39592  cdleme2  39593  cdleme3b  39594  cdleme3c  39595  cdleme3e  39597  cdleme9b  39617  cdlemedb  39662  cdleme20zN  39666  cdleme19a  39668  cdlemf2  39927  tendoidcl  40134  dia1eldmN  40406  dialss  40411  dia1N  40418  diaglbN  40420  diaintclN  40423  docaclN  40489  doca2N  40491  djajN  40502  dibglbN  40531  dibintclN  40532  dihlsscpre  40599  dih2dimbALTN  40610  dih1  40651  dihglblem5apreN  40656  dihglblem5aN  40657  dihglblem2aN  40658  dihmeetcl  40710  dochvalr  40722  djhlj  40766