Theorem hllat 40170

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Latclat 18505  AtLatcal 40071  HLchlt 40157

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-dm 5673  df-iota 6496  df-fv 6548  df-ov 7419  df-atl 40105  df-cvlat 40129  df-hlat 40158

This theorem is used by:  hllatd  40171  hlpos  40173  hlatjcl  40174  hlatjcom  40175  hlatjidm  40176  hlatjass  40177  hlatj32  40179  hlatj4  40181  hlatlej1  40182  atnlej1  40186  atnlej2  40187  hlateq  40206  hlrelat5N  40208  hlrelat2  40210  cvr2N  40218  cvrval5  40222  cvrexchlem  40226  cvrexch  40227  cvratlem  40228  cvrat  40229  cvrat2  40236  atcvrj2b  40239  atltcvr  40242  atlelt  40245  cvrat3  40249  cvrat4  40250  cvrat42  40251  2atjm  40252  3noncolr2  40256  3dimlem3OLDN  40269  3dimlem4OLDN  40272  1cvrat  40283  ps-1  40284  ps-2  40285  hlatexch3N  40287  3at  40297  llnneat  40321  lplni2  40344  2atnelpln  40351  lplnneat  40352  lplnnelln  40353  islpln2a  40355  2lplnmN  40366  2llnmj  40367  2llnm2N  40375  2llnm3N  40376  2llnm4  40377  2llnmeqat  40378  islvol5  40386  3atnelvolN  40393  lvolneatN  40395  lvolnelln  40396  lvolnelpln  40397  2lplnm2N  40428  2lplnmj  40429  pmap11  40569  isline3  40583  lncvrelatN  40588  2atm2atN  40592  2llnma1b  40593  2llnma3r  40595  paddasslem16  40642  paddass  40645  padd12N  40646  pmod2iN  40656  pmodN  40657  pmapjat1  40660  pmapjat2  40661  pmapjlln1  40662  hlmod1i  40663  atmod2i1  40668  atmod2i2  40669  atmod3i1  40671  atmod3i2  40672  atmod4i1  40673  atmod4i2  40674  llnexch2N  40677  polsubN  40714  paddunN  40734  pmapj2N  40736  pmapocjN  40737  psubclinN  40755  paddatclN  40756  linepsubclN  40758  lhpocnle  40823  lhpjat2  40828  lhpmcvr  40830  lhpm0atN  40836  lhpmatb  40838  trlval2  40970  trlcl  40971  trlle  40991  cdlemd1  41005  cdleme0cp  41021  cdleme0cq  41022  cdleme1b  41033  cdleme1  41034  cdleme2  41035  cdleme3b  41036  cdleme3c  41037  cdleme3e  41039  cdleme9b  41059  cdlemedb  41104  cdleme20zN  41108  cdleme19a  41110  cdlemf2  41369  tendoidcl  41576  dia1eldmN  41848  dialss  41853  dia1N  41860  diaglbN  41862  diaintclN  41865  docaclN  41931  doca2N  41933  djajN  41944  dibglbN  41973  dibintclN  41974  dihlsscpre  42041  dih2dimbALTN  42052  dih1  42093  dihglblem5apreN  42098  dihglblem5aN  42099  dihglblem2aN  42100  dihmeetcl  42152  dochvalr  42164  djhlj  42208