Theorem hllat 36498

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

Syntax hints:   → wi 4   ∈ wcel 2110  Latclat 17654  AtLatcal 36399  HLchlt 36485

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 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-dm 5564  df-iota 6313  df-fv 6362  df-ov 7158  df-atl 36433  df-cvlat 36457  df-hlat 36486

This theorem is referenced by:  hllatd  36499  hlpos  36501  hlatjcl  36502  hlatjcom  36503  hlatjidm  36504  hlatjass  36505  hlatj32  36507  hlatj4  36509  hlatlej1  36510  atnlej1  36514  atnlej2  36515  hlateq  36534  hlrelat5N  36536  hlrelat2  36538  cvr2N  36546  cvrval5  36550  cvrexchlem  36554  cvrexch  36555  cvratlem  36556  cvrat  36557  cvrat2  36564  atcvrj2b  36567  atltcvr  36570  atlelt  36573  cvrat3  36577  cvrat4  36578  cvrat42  36579  2atjm  36580  3noncolr2  36584  3dimlem3OLDN  36597  3dimlem4OLDN  36600  1cvrat  36611  ps-1  36612  ps-2  36613  hlatexch3N  36615  3at  36625  llnneat  36649  lplni2  36672  2atnelpln  36679  lplnneat  36680  lplnnelln  36681  islpln2a  36683  2lplnmN  36694  2llnmj  36695  2llnm2N  36703  2llnm3N  36704  2llnm4  36705  2llnmeqat  36706  islvol5  36714  3atnelvolN  36721  lvolneatN  36723  lvolnelln  36724  lvolnelpln  36725  2lplnm2N  36756  2lplnmj  36757  pmap11  36897  isline3  36911  lncvrelatN  36916  2atm2atN  36920  2llnma1b  36921  2llnma3r  36923  paddasslem16  36970  paddass  36973  padd12N  36974  pmod2iN  36984  pmodN  36985  pmapjat1  36988  pmapjat2  36989  pmapjlln1  36990  hlmod1i  36991  atmod2i1  36996  atmod2i2  36997  atmod3i1  36999  atmod3i2  37000  atmod4i1  37001  atmod4i2  37002  llnexch2N  37005  polsubN  37042  paddunN  37062  pmapj2N  37064  pmapocjN  37065  psubclinN  37083  paddatclN  37084  linepsubclN  37086  lhpocnle  37151  lhpjat2  37156  lhpmcvr  37158  lhpm0atN  37164  lhpmatb  37166  trlval2  37298  trlcl  37299  trlle  37319  cdlemd1  37333  cdleme0cp  37349  cdleme0cq  37350  cdleme1b  37361  cdleme1  37362  cdleme2  37363  cdleme3b  37364  cdleme3c  37365  cdleme3e  37367  cdleme9b  37387  cdlemedb  37432  cdleme20zN  37436  cdleme19a  37438  cdlemf2  37697  tendoidcl  37904  dia1eldmN  38176  dialss  38181  dia1N  38188  diaglbN  38190  diaintclN  38193  docaclN  38259  doca2N  38261  djajN  38272  dibglbN  38301  dibintclN  38302  dihlsscpre  38369  dih2dimbALTN  38380  dih1  38421  dihglblem5apreN  38426  dihglblem5aN  38427  dihglblem2aN  38428  dihmeetcl  38480  dochvalr  38492  djhlj  38536