Theorem hllat 39809

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

Syntax hints:   → wi 4   ∈ wcel 2114  Latclat 18397  AtLatcal 39710  HLchlt 39796

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-dm 5641  df-iota 6454  df-fv 6506  df-ov 7370  df-atl 39744  df-cvlat 39768  df-hlat 39797

This theorem is referenced by:  hllatd  39810  hlpos  39812  hlatjcl  39813  hlatjcom  39814  hlatjidm  39815  hlatjass  39816  hlatj32  39818  hlatj4  39820  hlatlej1  39821  atnlej1  39825  atnlej2  39826  hlateq  39845  hlrelat5N  39847  hlrelat2  39849  cvr2N  39857  cvrval5  39861  cvrexchlem  39865  cvrexch  39866  cvratlem  39867  cvrat  39868  cvrat2  39875  atcvrj2b  39878  atltcvr  39881  atlelt  39884  cvrat3  39888  cvrat4  39889  cvrat42  39890  2atjm  39891  3noncolr2  39895  3dimlem3OLDN  39908  3dimlem4OLDN  39911  1cvrat  39922  ps-1  39923  ps-2  39924  hlatexch3N  39926  3at  39936  llnneat  39960  lplni2  39983  2atnelpln  39990  lplnneat  39991  lplnnelln  39992  islpln2a  39994  2lplnmN  40005  2llnmj  40006  2llnm2N  40014  2llnm3N  40015  2llnm4  40016  2llnmeqat  40017  islvol5  40025  3atnelvolN  40032  lvolneatN  40034  lvolnelln  40035  lvolnelpln  40036  2lplnm2N  40067  2lplnmj  40068  pmap11  40208  isline3  40222  lncvrelatN  40227  2atm2atN  40231  2llnma1b  40232  2llnma3r  40234  paddasslem16  40281  paddass  40284  padd12N  40285  pmod2iN  40295  pmodN  40296  pmapjat1  40299  pmapjat2  40300  pmapjlln1  40301  hlmod1i  40302  atmod2i1  40307  atmod2i2  40308  atmod3i1  40310  atmod3i2  40311  atmod4i1  40312  atmod4i2  40313  llnexch2N  40316  polsubN  40353  paddunN  40373  pmapj2N  40375  pmapocjN  40376  psubclinN  40394  paddatclN  40395  linepsubclN  40397  lhpocnle  40462  lhpjat2  40467  lhpmcvr  40469  lhpm0atN  40475  lhpmatb  40477  trlval2  40609  trlcl  40610  trlle  40630  cdlemd1  40644  cdleme0cp  40660  cdleme0cq  40661  cdleme1b  40672  cdleme1  40673  cdleme2  40674  cdleme3b  40675  cdleme3c  40676  cdleme3e  40678  cdleme9b  40698  cdlemedb  40743  cdleme20zN  40747  cdleme19a  40749  cdlemf2  41008  tendoidcl  41215  dia1eldmN  41487  dialss  41492  dia1N  41499  diaglbN  41501  diaintclN  41504  docaclN  41570  doca2N  41572  djajN  41583  dibglbN  41612  dibintclN  41613  dihlsscpre  41680  dih2dimbALTN  41691  dih1  41732  dihglblem5apreN  41737  dihglblem5aN  41738  dihglblem2aN  41739  dihmeetcl  41791  dochvalr  41803  djhlj  41847