Theorem hllat 36514

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

Syntax hints:   → wi 4   ∈ wcel 2114  Latclat 17655  AtLatcal 36415  HLchlt 36501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-dm 5565  df-iota 6314  df-fv 6363  df-ov 7159  df-atl 36449  df-cvlat 36473  df-hlat 36502

This theorem is referenced by:  hllatd  36515  hlpos  36517  hlatjcl  36518  hlatjcom  36519  hlatjidm  36520  hlatjass  36521  hlatj32  36523  hlatj4  36525  hlatlej1  36526  atnlej1  36530  atnlej2  36531  hlateq  36550  hlrelat5N  36552  hlrelat2  36554  cvr2N  36562  cvrval5  36566  cvrexchlem  36570  cvrexch  36571  cvratlem  36572  cvrat  36573  cvrat2  36580  atcvrj2b  36583  atltcvr  36586  atlelt  36589  cvrat3  36593  cvrat4  36594  cvrat42  36595  2atjm  36596  3noncolr2  36600  3dimlem3OLDN  36613  3dimlem4OLDN  36616  1cvrat  36627  ps-1  36628  ps-2  36629  hlatexch3N  36631  3at  36641  llnneat  36665  lplni2  36688  2atnelpln  36695  lplnneat  36696  lplnnelln  36697  islpln2a  36699  2lplnmN  36710  2llnmj  36711  2llnm2N  36719  2llnm3N  36720  2llnm4  36721  2llnmeqat  36722  islvol5  36730  3atnelvolN  36737  lvolneatN  36739  lvolnelln  36740  lvolnelpln  36741  2lplnm2N  36772  2lplnmj  36773  pmap11  36913  isline3  36927  lncvrelatN  36932  2atm2atN  36936  2llnma1b  36937  2llnma3r  36939  paddasslem16  36986  paddass  36989  padd12N  36990  pmod2iN  37000  pmodN  37001  pmapjat1  37004  pmapjat2  37005  pmapjlln1  37006  hlmod1i  37007  atmod2i1  37012  atmod2i2  37013  atmod3i1  37015  atmod3i2  37016  atmod4i1  37017  atmod4i2  37018  llnexch2N  37021  polsubN  37058  paddunN  37078  pmapj2N  37080  pmapocjN  37081  psubclinN  37099  paddatclN  37100  linepsubclN  37102  lhpocnle  37167  lhpjat2  37172  lhpmcvr  37174  lhpm0atN  37180  lhpmatb  37182  trlval2  37314  trlcl  37315  trlle  37335  cdlemd1  37349  cdleme0cp  37365  cdleme0cq  37366  cdleme1b  37377  cdleme1  37378  cdleme2  37379  cdleme3b  37380  cdleme3c  37381  cdleme3e  37383  cdleme9b  37403  cdlemedb  37448  cdleme20zN  37452  cdleme19a  37454  cdlemf2  37713  tendoidcl  37920  dia1eldmN  38192  dialss  38197  dia1N  38204  diaglbN  38206  diaintclN  38209  docaclN  38275  doca2N  38277  djajN  38288  dibglbN  38317  dibintclN  38318  dihlsscpre  38385  dih2dimbALTN  38396  dih1  38437  dihglblem5apreN  38442  dihglblem5aN  38443  dihglblem2aN  38444  dihmeetcl  38496  dochvalr  38508  djhlj  38552