Theorem hllat 36659

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

Syntax hints:   → wi 4   ∈ wcel 2111  Latclat 17647  AtLatcal 36560  HLchlt 36646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-dm 5529  df-iota 6283  df-fv 6332  df-ov 7138  df-atl 36594  df-cvlat 36618  df-hlat 36647

This theorem is referenced by:  hllatd  36660  hlpos  36662  hlatjcl  36663  hlatjcom  36664  hlatjidm  36665  hlatjass  36666  hlatj32  36668  hlatj4  36670  hlatlej1  36671  atnlej1  36675  atnlej2  36676  hlateq  36695  hlrelat5N  36697  hlrelat2  36699  cvr2N  36707  cvrval5  36711  cvrexchlem  36715  cvrexch  36716  cvratlem  36717  cvrat  36718  cvrat2  36725  atcvrj2b  36728  atltcvr  36731  atlelt  36734  cvrat3  36738  cvrat4  36739  cvrat42  36740  2atjm  36741  3noncolr2  36745  3dimlem3OLDN  36758  3dimlem4OLDN  36761  1cvrat  36772  ps-1  36773  ps-2  36774  hlatexch3N  36776  3at  36786  llnneat  36810  lplni2  36833  2atnelpln  36840  lplnneat  36841  lplnnelln  36842  islpln2a  36844  2lplnmN  36855  2llnmj  36856  2llnm2N  36864  2llnm3N  36865  2llnm4  36866  2llnmeqat  36867  islvol5  36875  3atnelvolN  36882  lvolneatN  36884  lvolnelln  36885  lvolnelpln  36886  2lplnm2N  36917  2lplnmj  36918  pmap11  37058  isline3  37072  lncvrelatN  37077  2atm2atN  37081  2llnma1b  37082  2llnma3r  37084  paddasslem16  37131  paddass  37134  padd12N  37135  pmod2iN  37145  pmodN  37146  pmapjat1  37149  pmapjat2  37150  pmapjlln1  37151  hlmod1i  37152  atmod2i1  37157  atmod2i2  37158  atmod3i1  37160  atmod3i2  37161  atmod4i1  37162  atmod4i2  37163  llnexch2N  37166  polsubN  37203  paddunN  37223  pmapj2N  37225  pmapocjN  37226  psubclinN  37244  paddatclN  37245  linepsubclN  37247  lhpocnle  37312  lhpjat2  37317  lhpmcvr  37319  lhpm0atN  37325  lhpmatb  37327  trlval2  37459  trlcl  37460  trlle  37480  cdlemd1  37494  cdleme0cp  37510  cdleme0cq  37511  cdleme1b  37522  cdleme1  37523  cdleme2  37524  cdleme3b  37525  cdleme3c  37526  cdleme3e  37528  cdleme9b  37548  cdlemedb  37593  cdleme20zN  37597  cdleme19a  37599  cdlemf2  37858  tendoidcl  38065  dia1eldmN  38337  dialss  38342  dia1N  38349  diaglbN  38351  diaintclN  38354  docaclN  38420  doca2N  38422  djajN  38433  dibglbN  38462  dibintclN  38463  dihlsscpre  38530  dih2dimbALTN  38541  dih1  38582  dihglblem5apreN  38587  dihglblem5aN  38588  dihglblem2aN  38589  dihmeetcl  38641  dochvalr  38653  djhlj  38697