Theorem hllat 40022

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

Syntax hints:   → wi 4   ∈ wcel 2149  Latclat 18483  AtLatcal 39923  HLchlt 40009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-dm 5669  df-iota 6489  df-fv 6541  df-ov 7411  df-atl 39957  df-cvlat 39981  df-hlat 40010

This theorem is referenced by:  hllatd  40023  hlpos  40025  hlatjcl  40026  hlatjcom  40027  hlatjidm  40028  hlatjass  40029  hlatj32  40031  hlatj4  40033  hlatlej1  40034  atnlej1  40038  atnlej2  40039  hlateq  40058  hlrelat5N  40060  hlrelat2  40062  cvr2N  40070  cvrval5  40074  cvrexchlem  40078  cvrexch  40079  cvratlem  40080  cvrat  40081  cvrat2  40088  atcvrj2b  40091  atltcvr  40094  atlelt  40097  cvrat3  40101  cvrat4  40102  cvrat42  40103  2atjm  40104  3noncolr2  40108  3dimlem3OLDN  40121  3dimlem4OLDN  40124  1cvrat  40135  ps-1  40136  ps-2  40137  hlatexch3N  40139  3at  40149  llnneat  40173  lplni2  40196  2atnelpln  40203  lplnneat  40204  lplnnelln  40205  islpln2a  40207  2lplnmN  40218  2llnmj  40219  2llnm2N  40227  2llnm3N  40228  2llnm4  40229  2llnmeqat  40230  islvol5  40238  3atnelvolN  40245  lvolneatN  40247  lvolnelln  40248  lvolnelpln  40249  2lplnm2N  40280  2lplnmj  40281  pmap11  40421  isline3  40435  lncvrelatN  40440  2atm2atN  40444  2llnma1b  40445  2llnma3r  40447  paddasslem16  40494  paddass  40497  padd12N  40498  pmod2iN  40508  pmodN  40509  pmapjat1  40512  pmapjat2  40513  pmapjlln1  40514  hlmod1i  40515  atmod2i1  40520  atmod2i2  40521  atmod3i1  40523  atmod3i2  40524  atmod4i1  40525  atmod4i2  40526  llnexch2N  40529  polsubN  40566  paddunN  40586  pmapj2N  40588  pmapocjN  40589  psubclinN  40607  paddatclN  40608  linepsubclN  40610  lhpocnle  40675  lhpjat2  40680  lhpmcvr  40682  lhpm0atN  40688  lhpmatb  40690  trlval2  40822  trlcl  40823  trlle  40843  cdlemd1  40857  cdleme0cp  40873  cdleme0cq  40874  cdleme1b  40885  cdleme1  40886  cdleme2  40887  cdleme3b  40888  cdleme3c  40889  cdleme3e  40891  cdleme9b  40911  cdlemedb  40956  cdleme20zN  40960  cdleme19a  40962  cdlemf2  41221  tendoidcl  41428  dia1eldmN  41700  dialss  41705  dia1N  41712  diaglbN  41714  diaintclN  41717  docaclN  41783  doca2N  41785  djajN  41796  dibglbN  41825  dibintclN  41826  dihlsscpre  41893  dih2dimbALTN  41904  dih1  41945  dihglblem5apreN  41950  dihglblem5aN  41951  dihglblem2aN  41952  dihmeetcl  42004  dochvalr  42016  djhlj  42060