Theorem hllat 39361

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

Syntax hints:   → wi 4   ∈ wcel 2109  Latclat 18356  AtLatcal 39262  HLchlt 39348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-dm 5633  df-iota 6442  df-fv 6494  df-ov 7356  df-atl 39296  df-cvlat 39320  df-hlat 39349

This theorem is referenced by:  hllatd  39362  hlpos  39364  hlatjcl  39365  hlatjcom  39366  hlatjidm  39367  hlatjass  39368  hlatj32  39370  hlatj4  39372  hlatlej1  39373  atnlej1  39378  atnlej2  39379  hlateq  39398  hlrelat5N  39400  hlrelat2  39402  cvr2N  39410  cvrval5  39414  cvrexchlem  39418  cvrexch  39419  cvratlem  39420  cvrat  39421  cvrat2  39428  atcvrj2b  39431  atltcvr  39434  atlelt  39437  cvrat3  39441  cvrat4  39442  cvrat42  39443  2atjm  39444  3noncolr2  39448  3dimlem3OLDN  39461  3dimlem4OLDN  39464  1cvrat  39475  ps-1  39476  ps-2  39477  hlatexch3N  39479  3at  39489  llnneat  39513  lplni2  39536  2atnelpln  39543  lplnneat  39544  lplnnelln  39545  islpln2a  39547  2lplnmN  39558  2llnmj  39559  2llnm2N  39567  2llnm3N  39568  2llnm4  39569  2llnmeqat  39570  islvol5  39578  3atnelvolN  39585  lvolneatN  39587  lvolnelln  39588  lvolnelpln  39589  2lplnm2N  39620  2lplnmj  39621  pmap11  39761  isline3  39775  lncvrelatN  39780  2atm2atN  39784  2llnma1b  39785  2llnma3r  39787  paddasslem16  39834  paddass  39837  padd12N  39838  pmod2iN  39848  pmodN  39849  pmapjat1  39852  pmapjat2  39853  pmapjlln1  39854  hlmod1i  39855  atmod2i1  39860  atmod2i2  39861  atmod3i1  39863  atmod3i2  39864  atmod4i1  39865  atmod4i2  39866  llnexch2N  39869  polsubN  39906  paddunN  39926  pmapj2N  39928  pmapocjN  39929  psubclinN  39947  paddatclN  39948  linepsubclN  39950  lhpocnle  40015  lhpjat2  40020  lhpmcvr  40022  lhpm0atN  40028  lhpmatb  40030  trlval2  40162  trlcl  40163  trlle  40183  cdlemd1  40197  cdleme0cp  40213  cdleme0cq  40214  cdleme1b  40225  cdleme1  40226  cdleme2  40227  cdleme3b  40228  cdleme3c  40229  cdleme3e  40231  cdleme9b  40251  cdlemedb  40296  cdleme20zN  40300  cdleme19a  40302  cdlemf2  40561  tendoidcl  40768  dia1eldmN  41040  dialss  41045  dia1N  41052  diaglbN  41054  diaintclN  41057  docaclN  41123  doca2N  41125  djajN  41136  dibglbN  41165  dibintclN  41166  dihlsscpre  41233  dih2dimbALTN  41244  dih1  41285  dihglblem5apreN  41290  dihglblem5aN  41291  dihglblem2aN  41292  dihmeetcl  41344  dochvalr  41356  djhlj  41400