Theorem hllat 39351

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

Syntax hints:   → wi 4   ∈ wcel 2109  Latclat 18396  AtLatcal 39252  HLchlt 39338

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-dm 5650  df-iota 6466  df-fv 6521  df-ov 7392  df-atl 39286  df-cvlat 39310  df-hlat 39339

This theorem is referenced by:  hllatd  39352  hlpos  39354  hlatjcl  39355  hlatjcom  39356  hlatjidm  39357  hlatjass  39358  hlatj32  39360  hlatj4  39362  hlatlej1  39363  atnlej1  39368  atnlej2  39369  hlateq  39388  hlrelat5N  39390  hlrelat2  39392  cvr2N  39400  cvrval5  39404  cvrexchlem  39408  cvrexch  39409  cvratlem  39410  cvrat  39411  cvrat2  39418  atcvrj2b  39421  atltcvr  39424  atlelt  39427  cvrat3  39431  cvrat4  39432  cvrat42  39433  2atjm  39434  3noncolr2  39438  3dimlem3OLDN  39451  3dimlem4OLDN  39454  1cvrat  39465  ps-1  39466  ps-2  39467  hlatexch3N  39469  3at  39479  llnneat  39503  lplni2  39526  2atnelpln  39533  lplnneat  39534  lplnnelln  39535  islpln2a  39537  2lplnmN  39548  2llnmj  39549  2llnm2N  39557  2llnm3N  39558  2llnm4  39559  2llnmeqat  39560  islvol5  39568  3atnelvolN  39575  lvolneatN  39577  lvolnelln  39578  lvolnelpln  39579  2lplnm2N  39610  2lplnmj  39611  pmap11  39751  isline3  39765  lncvrelatN  39770  2atm2atN  39774  2llnma1b  39775  2llnma3r  39777  paddasslem16  39824  paddass  39827  padd12N  39828  pmod2iN  39838  pmodN  39839  pmapjat1  39842  pmapjat2  39843  pmapjlln1  39844  hlmod1i  39845  atmod2i1  39850  atmod2i2  39851  atmod3i1  39853  atmod3i2  39854  atmod4i1  39855  atmod4i2  39856  llnexch2N  39859  polsubN  39896  paddunN  39916  pmapj2N  39918  pmapocjN  39919  psubclinN  39937  paddatclN  39938  linepsubclN  39940  lhpocnle  40005  lhpjat2  40010  lhpmcvr  40012  lhpm0atN  40018  lhpmatb  40020  trlval2  40152  trlcl  40153  trlle  40173  cdlemd1  40187  cdleme0cp  40203  cdleme0cq  40204  cdleme1b  40215  cdleme1  40216  cdleme2  40217  cdleme3b  40218  cdleme3c  40219  cdleme3e  40221  cdleme9b  40241  cdlemedb  40286  cdleme20zN  40290  cdleme19a  40292  cdlemf2  40551  tendoidcl  40758  dia1eldmN  41030  dialss  41035  dia1N  41042  diaglbN  41044  diaintclN  41047  docaclN  41113  doca2N  41115  djajN  41126  dibglbN  41155  dibintclN  41156  dihlsscpre  41223  dih2dimbALTN  41234  dih1  41275  dihglblem5apreN  41280  dihglblem5aN  41281  dihglblem2aN  41282  dihmeetcl  41334  dochvalr  41346  djhlj  41390