Theorem hllat 39535

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

Syntax hints:   → wi 4   ∈ wcel 2113  Latclat 18345  AtLatcal 39436  HLchlt 39522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-dm 5631  df-iota 6445  df-fv 6497  df-ov 7358  df-atl 39470  df-cvlat 39494  df-hlat 39523

This theorem is referenced by:  hllatd  39536  hlpos  39538  hlatjcl  39539  hlatjcom  39540  hlatjidm  39541  hlatjass  39542  hlatj32  39544  hlatj4  39546  hlatlej1  39547  atnlej1  39551  atnlej2  39552  hlateq  39571  hlrelat5N  39573  hlrelat2  39575  cvr2N  39583  cvrval5  39587  cvrexchlem  39591  cvrexch  39592  cvratlem  39593  cvrat  39594  cvrat2  39601  atcvrj2b  39604  atltcvr  39607  atlelt  39610  cvrat3  39614  cvrat4  39615  cvrat42  39616  2atjm  39617  3noncolr2  39621  3dimlem3OLDN  39634  3dimlem4OLDN  39637  1cvrat  39648  ps-1  39649  ps-2  39650  hlatexch3N  39652  3at  39662  llnneat  39686  lplni2  39709  2atnelpln  39716  lplnneat  39717  lplnnelln  39718  islpln2a  39720  2lplnmN  39731  2llnmj  39732  2llnm2N  39740  2llnm3N  39741  2llnm4  39742  2llnmeqat  39743  islvol5  39751  3atnelvolN  39758  lvolneatN  39760  lvolnelln  39761  lvolnelpln  39762  2lplnm2N  39793  2lplnmj  39794  pmap11  39934  isline3  39948  lncvrelatN  39953  2atm2atN  39957  2llnma1b  39958  2llnma3r  39960  paddasslem16  40007  paddass  40010  padd12N  40011  pmod2iN  40021  pmodN  40022  pmapjat1  40025  pmapjat2  40026  pmapjlln1  40027  hlmod1i  40028  atmod2i1  40033  atmod2i2  40034  atmod3i1  40036  atmod3i2  40037  atmod4i1  40038  atmod4i2  40039  llnexch2N  40042  polsubN  40079  paddunN  40099  pmapj2N  40101  pmapocjN  40102  psubclinN  40120  paddatclN  40121  linepsubclN  40123  lhpocnle  40188  lhpjat2  40193  lhpmcvr  40195  lhpm0atN  40201  lhpmatb  40203  trlval2  40335  trlcl  40336  trlle  40356  cdlemd1  40370  cdleme0cp  40386  cdleme0cq  40387  cdleme1b  40398  cdleme1  40399  cdleme2  40400  cdleme3b  40401  cdleme3c  40402  cdleme3e  40404  cdleme9b  40424  cdlemedb  40469  cdleme20zN  40473  cdleme19a  40475  cdlemf2  40734  tendoidcl  40941  dia1eldmN  41213  dialss  41218  dia1N  41225  diaglbN  41227  diaintclN  41230  docaclN  41296  doca2N  41298  djajN  41309  dibglbN  41338  dibintclN  41339  dihlsscpre  41406  dih2dimbALTN  41417  dih1  41458  dihglblem5apreN  41463  dihglblem5aN  41464  dihglblem2aN  41465  dihmeetcl  41517  dochvalr  41529  djhlj  41573