Theorem hllat 40400

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Latclat 18598  AtLatcal 40301  HLchlt 40387

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-dm 5661  df-iota 6493  df-fv 6545  df-ov 7421  df-atl 40335  df-cvlat 40359  df-hlat 40388

This theorem is used by:  hllatd  40401  hlpos  40403  hlatjcl  40404  hlatjcom  40405  hlatjidm  40406  hlatjass  40407  hlatj32  40409  hlatj4  40411  hlatlej1  40412  atnlej1  40416  atnlej2  40417  hlateq  40436  hlrelat5N  40438  hlrelat2  40440  cvr2N  40448  cvrval5  40452  cvrexchlem  40456  cvrexch  40457  cvratlem  40458  cvrat  40459  cvrat2  40466  atcvrj2b  40469  atltcvr  40472  atlelt  40475  cvrat3  40479  cvrat4  40480  cvrat42  40481  2atjm  40482  3noncolr2  40486  3dimlem3OLDN  40499  3dimlem4OLDN  40502  1cvrat  40513  ps-1  40514  ps-2  40515  hlatexch3N  40517  3at  40527  llnneat  40551  lplni2  40574  2atnelpln  40581  lplnneat  40582  lplnnelln  40583  islpln2a  40585  2lplnmN  40596  2llnmj  40597  2llnm2N  40605  2llnm3N  40606  2llnm4  40607  2llnmeqat  40608  islvol5  40616  3atnelvolN  40623  lvolneatN  40625  lvolnelln  40626  lvolnelpln  40627  2lplnm2N  40658  2lplnmj  40659  pmap11  40799  isline3  40813  lncvrelatN  40818  2atm2atN  40822  2llnma1b  40823  2llnma3r  40825  paddasslem16  40872  paddass  40875  padd12N  40876  pmod2iN  40886  pmodN  40887  pmapjat1  40890  pmapjat2  40891  pmapjlln1  40892  hlmod1i  40893  atmod2i1  40898  atmod2i2  40899  atmod3i1  40901  atmod3i2  40902  atmod4i1  40903  atmod4i2  40904  llnexch2N  40907  polsubN  40944  paddunN  40964  pmapj2N  40966  pmapocjN  40967  psubclinN  40985  paddatclN  40986  linepsubclN  40988  lhpocnle  41053  lhpjat2  41058  lhpmcvr  41060  lhpm0atN  41066  lhpmatb  41068  trlval2  41200  trlcl  41201  trlle  41221  cdlemd1  41235  cdleme0cp  41251  cdleme0cq  41252  cdleme1b  41263  cdleme1  41264  cdleme2  41265  cdleme3b  41266  cdleme3c  41267  cdleme3e  41269  cdleme9b  41289  cdlemedb  41334  cdleme20zN  41338  cdleme19a  41340  cdlemf2  41599  tendoidcl  41806  dia1eldmN  42078  dialss  42083  dia1N  42090  diaglbN  42092  diaintclN  42095  docaclN  42161  doca2N  42163  djajN  42174  dibglbN  42203  dibintclN  42204  dihlsscpre  42271  dih2dimbALTN  42282  dih1  42323  dihglblem5apreN  42328  dihglblem5aN  42329  dihglblem2aN  42330  dihmeetcl  42382  dochvalr  42394  djhlj  42438