Theorem hllat 39363

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

Syntax hints:   → wi 4   ∈ wcel 2109  Latclat 18397  AtLatcal 39264  HLchlt 39350

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 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-dm 5651  df-iota 6467  df-fv 6522  df-ov 7393  df-atl 39298  df-cvlat 39322  df-hlat 39351

This theorem is referenced by:  hllatd  39364  hlpos  39366  hlatjcl  39367  hlatjcom  39368  hlatjidm  39369  hlatjass  39370  hlatj32  39372  hlatj4  39374  hlatlej1  39375  atnlej1  39380  atnlej2  39381  hlateq  39400  hlrelat5N  39402  hlrelat2  39404  cvr2N  39412  cvrval5  39416  cvrexchlem  39420  cvrexch  39421  cvratlem  39422  cvrat  39423  cvrat2  39430  atcvrj2b  39433  atltcvr  39436  atlelt  39439  cvrat3  39443  cvrat4  39444  cvrat42  39445  2atjm  39446  3noncolr2  39450  3dimlem3OLDN  39463  3dimlem4OLDN  39466  1cvrat  39477  ps-1  39478  ps-2  39479  hlatexch3N  39481  3at  39491  llnneat  39515  lplni2  39538  2atnelpln  39545  lplnneat  39546  lplnnelln  39547  islpln2a  39549  2lplnmN  39560  2llnmj  39561  2llnm2N  39569  2llnm3N  39570  2llnm4  39571  2llnmeqat  39572  islvol5  39580  3atnelvolN  39587  lvolneatN  39589  lvolnelln  39590  lvolnelpln  39591  2lplnm2N  39622  2lplnmj  39623  pmap11  39763  isline3  39777  lncvrelatN  39782  2atm2atN  39786  2llnma1b  39787  2llnma3r  39789  paddasslem16  39836  paddass  39839  padd12N  39840  pmod2iN  39850  pmodN  39851  pmapjat1  39854  pmapjat2  39855  pmapjlln1  39856  hlmod1i  39857  atmod2i1  39862  atmod2i2  39863  atmod3i1  39865  atmod3i2  39866  atmod4i1  39867  atmod4i2  39868  llnexch2N  39871  polsubN  39908  paddunN  39928  pmapj2N  39930  pmapocjN  39931  psubclinN  39949  paddatclN  39950  linepsubclN  39952  lhpocnle  40017  lhpjat2  40022  lhpmcvr  40024  lhpm0atN  40030  lhpmatb  40032  trlval2  40164  trlcl  40165  trlle  40185  cdlemd1  40199  cdleme0cp  40215  cdleme0cq  40216  cdleme1b  40227  cdleme1  40228  cdleme2  40229  cdleme3b  40230  cdleme3c  40231  cdleme3e  40233  cdleme9b  40253  cdlemedb  40298  cdleme20zN  40302  cdleme19a  40304  cdlemf2  40563  tendoidcl  40770  dia1eldmN  41042  dialss  41047  dia1N  41054  diaglbN  41056  diaintclN  41059  docaclN  41125  doca2N  41127  djajN  41138  dibglbN  41167  dibintclN  41168  dihlsscpre  41235  dih2dimbALTN  41246  dih1  41287  dihglblem5apreN  41292  dihglblem5aN  41293  dihglblem2aN  41294  dihmeetcl  41346  dochvalr  41358  djhlj  41402