Theorem hllat 40514

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Latclat 18611  AtLatcal 40415  HLchlt 40501

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-dm 5660  df-iota 6494  df-fv 6547  df-ov 7424  df-atl 40449  df-cvlat 40473  df-hlat 40502

This theorem is used by:  hllatd  40515  hlpos  40517  hlatjcl  40518  hlatjcom  40519  hlatjidm  40520  hlatjass  40521  hlatj32  40523  hlatj4  40525  hlatlej1  40526  atnlej1  40530  atnlej2  40531  hlateq  40550  hlrelat5N  40552  hlrelat2  40554  cvr2N  40562  cvrval5  40566  cvrexchlem  40570  cvrexch  40571  cvratlem  40572  cvrat  40573  cvrat2  40580  atcvrj2b  40583  atltcvr  40586  atlelt  40589  cvrat3  40593  cvrat4  40594  cvrat42  40595  2atjm  40596  3noncolr2  40600  3dimlem3OLDN  40613  3dimlem4OLDN  40616  1cvrat  40627  ps-1  40628  ps-2  40629  hlatexch3N  40631  3at  40641  llnneat  40665  lplni2  40688  2atnelpln  40695  lplnneat  40696  lplnnelln  40697  islpln2a  40699  2lplnmN  40710  2llnmj  40711  2llnm2N  40719  2llnm3N  40720  2llnm4  40721  2llnmeqat  40722  islvol5  40730  3atnelvolN  40737  lvolneatN  40739  lvolnelln  40740  lvolnelpln  40741  2lplnm2N  40772  2lplnmj  40773  pmap11  40913  isline3  40927  lncvrelatN  40932  2atm2atN  40936  2llnma1b  40937  2llnma3r  40939  paddasslem16  40986  paddass  40989  padd12N  40990  pmod2iN  41000  pmodN  41001  pmapjat1  41004  pmapjat2  41005  pmapjlln1  41006  hlmod1i  41007  atmod2i1  41012  atmod2i2  41013  atmod3i1  41015  atmod3i2  41016  atmod4i1  41017  atmod4i2  41018  llnexch2N  41021  polsubN  41058  paddunN  41078  pmapj2N  41080  pmapocjN  41081  psubclinN  41099  paddatclN  41100  linepsubclN  41102  lhpocnle  41167  lhpjat2  41172  lhpmcvr  41174  lhpm0atN  41180  lhpmatb  41182  trlval2  41314  trlcl  41315  trlle  41335  cdlemd1  41349  cdleme0cp  41365  cdleme0cq  41366  cdleme1b  41377  cdleme1  41378  cdleme2  41379  cdleme3b  41380  cdleme3c  41381  cdleme3e  41383  cdleme9b  41403  cdlemedb  41448  cdleme20zN  41452  cdleme19a  41454  cdlemf2  41713  tendoidcl  41920  dia1eldmN  42192  dialss  42197  dia1N  42204  diaglbN  42206  diaintclN  42209  docaclN  42275  doca2N  42277  djajN  42288  dibglbN  42317  dibintclN  42318  dihlsscpre  42385  dih2dimbALTN  42396  dih1  42437  dihglblem5apreN  42442  dihglblem5aN  42443  dihglblem2aN  42444  dihmeetcl  42496  dochvalr  42508  djhlj  42552