Theorem hllat 39319

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

Syntax hints:   → wi 4   ∈ wcel 2108  Latclat 18501  AtLatcal 39220  HLchlt 39306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-dm 5710  df-iota 6525  df-fv 6581  df-ov 7451  df-atl 39254  df-cvlat 39278  df-hlat 39307

This theorem is referenced by:  hllatd  39320  hlpos  39322  hlatjcl  39323  hlatjcom  39324  hlatjidm  39325  hlatjass  39326  hlatj32  39328  hlatj4  39330  hlatlej1  39331  atnlej1  39336  atnlej2  39337  hlateq  39356  hlrelat5N  39358  hlrelat2  39360  cvr2N  39368  cvrval5  39372  cvrexchlem  39376  cvrexch  39377  cvratlem  39378  cvrat  39379  cvrat2  39386  atcvrj2b  39389  atltcvr  39392  atlelt  39395  cvrat3  39399  cvrat4  39400  cvrat42  39401  2atjm  39402  3noncolr2  39406  3dimlem3OLDN  39419  3dimlem4OLDN  39422  1cvrat  39433  ps-1  39434  ps-2  39435  hlatexch3N  39437  3at  39447  llnneat  39471  lplni2  39494  2atnelpln  39501  lplnneat  39502  lplnnelln  39503  islpln2a  39505  2lplnmN  39516  2llnmj  39517  2llnm2N  39525  2llnm3N  39526  2llnm4  39527  2llnmeqat  39528  islvol5  39536  3atnelvolN  39543  lvolneatN  39545  lvolnelln  39546  lvolnelpln  39547  2lplnm2N  39578  2lplnmj  39579  pmap11  39719  isline3  39733  lncvrelatN  39738  2atm2atN  39742  2llnma1b  39743  2llnma3r  39745  paddasslem16  39792  paddass  39795  padd12N  39796  pmod2iN  39806  pmodN  39807  pmapjat1  39810  pmapjat2  39811  pmapjlln1  39812  hlmod1i  39813  atmod2i1  39818  atmod2i2  39819  atmod3i1  39821  atmod3i2  39822  atmod4i1  39823  atmod4i2  39824  llnexch2N  39827  polsubN  39864  paddunN  39884  pmapj2N  39886  pmapocjN  39887  psubclinN  39905  paddatclN  39906  linepsubclN  39908  lhpocnle  39973  lhpjat2  39978  lhpmcvr  39980  lhpm0atN  39986  lhpmatb  39988  trlval2  40120  trlcl  40121  trlle  40141  cdlemd1  40155  cdleme0cp  40171  cdleme0cq  40172  cdleme1b  40183  cdleme1  40184  cdleme2  40185  cdleme3b  40186  cdleme3c  40187  cdleme3e  40189  cdleme9b  40209  cdlemedb  40254  cdleme20zN  40258  cdleme19a  40260  cdlemf2  40519  tendoidcl  40726  dia1eldmN  40998  dialss  41003  dia1N  41010  diaglbN  41012  diaintclN  41015  docaclN  41081  doca2N  41083  djajN  41094  dibglbN  41123  dibintclN  41124  dihlsscpre  41191  dih2dimbALTN  41202  dih1  41243  dihglblem5apreN  41248  dihglblem5aN  41249  dihglblem2aN  41250  dihmeetcl  41302  dochvalr  41314  djhlj  41358