Theorem hllat 40236

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Latclat 18519  AtLatcal 40137  HLchlt 40223

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5665  df-iota 6489  df-fv 6541  df-ov 7416  df-atl 40171  df-cvlat 40195  df-hlat 40224

This theorem is used by:  hllatd  40237  hlpos  40239  hlatjcl  40240  hlatjcom  40241  hlatjidm  40242  hlatjass  40243  hlatj32  40245  hlatj4  40247  hlatlej1  40248  atnlej1  40252  atnlej2  40253  hlateq  40272  hlrelat5N  40274  hlrelat2  40276  cvr2N  40284  cvrval5  40288  cvrexchlem  40292  cvrexch  40293  cvratlem  40294  cvrat  40295  cvrat2  40302  atcvrj2b  40305  atltcvr  40308  atlelt  40311  cvrat3  40315  cvrat4  40316  cvrat42  40317  2atjm  40318  3noncolr2  40322  3dimlem3OLDN  40335  3dimlem4OLDN  40338  1cvrat  40349  ps-1  40350  ps-2  40351  hlatexch3N  40353  3at  40363  llnneat  40387  lplni2  40410  2atnelpln  40417  lplnneat  40418  lplnnelln  40419  islpln2a  40421  2lplnmN  40432  2llnmj  40433  2llnm2N  40441  2llnm3N  40442  2llnm4  40443  2llnmeqat  40444  islvol5  40452  3atnelvolN  40459  lvolneatN  40461  lvolnelln  40462  lvolnelpln  40463  2lplnm2N  40494  2lplnmj  40495  pmap11  40635  isline3  40649  lncvrelatN  40654  2atm2atN  40658  2llnma1b  40659  2llnma3r  40661  paddasslem16  40708  paddass  40711  padd12N  40712  pmod2iN  40722  pmodN  40723  pmapjat1  40726  pmapjat2  40727  pmapjlln1  40728  hlmod1i  40729  atmod2i1  40734  atmod2i2  40735  atmod3i1  40737  atmod3i2  40738  atmod4i1  40739  atmod4i2  40740  llnexch2N  40743  polsubN  40780  paddunN  40800  pmapj2N  40802  pmapocjN  40803  psubclinN  40821  paddatclN  40822  linepsubclN  40824  lhpocnle  40889  lhpjat2  40894  lhpmcvr  40896  lhpm0atN  40902  lhpmatb  40904  trlval2  41036  trlcl  41037  trlle  41057  cdlemd1  41071  cdleme0cp  41087  cdleme0cq  41088  cdleme1b  41099  cdleme1  41100  cdleme2  41101  cdleme3b  41102  cdleme3c  41103  cdleme3e  41105  cdleme9b  41125  cdlemedb  41170  cdleme20zN  41174  cdleme19a  41176  cdlemf2  41435  tendoidcl  41642  dia1eldmN  41914  dialss  41919  dia1N  41926  diaglbN  41928  diaintclN  41931  docaclN  41997  doca2N  41999  djajN  42010  dibglbN  42039  dibintclN  42040  dihlsscpre  42107  dih2dimbALTN  42118  dih1  42159  dihglblem5apreN  42164  dihglblem5aN  42165  dihglblem2aN  42166  dihmeetcl  42218  dochvalr  42230  djhlj  42274