MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  latmcl Structured version   Visualization version   GIF version

Theorem latmcl 17277
Description: Closure of meet operation in a lattice. (incom 4015 analog.) (Contributed by NM, 14-Sep-2011.)
Hypotheses
Ref Expression
latmcl.b 𝐵 = (Base‘𝐾)
latmcl.m = (meet‘𝐾)
Assertion
Ref Expression
latmcl ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)

Proof of Theorem latmcl
StepHypRef Expression
1 latmcl.b . . 3 𝐵 = (Base‘𝐾)
2 eqid 2817 . . 3 (join‘𝐾) = (join‘𝐾)
3 latmcl.m . . 3 = (meet‘𝐾)
41, 2, 3latlem 17274 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ((𝑋(join‘𝐾)𝑌) ∈ 𝐵 ∧ (𝑋 𝑌) ∈ 𝐵))
54simprd 485 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1100   = wceq 1637  wcel 2157  cfv 6111  (class class class)co 6884  Basecbs 16088  joincjn 17169  meetcmee 17170  Latclat 17270
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4977  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-id 5232  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-riota 6845  df-ov 6887  df-oprab 6888  df-lub 17199  df-glb 17200  df-join 17201  df-meet 17202  df-lat 17271
This theorem is referenced by:  latleeqm1  17304  latmlem1  17306  latmlem12  17308  latnlemlt  17309  latmidm  17311  latabs1  17312  latledi  17314  latmlej11  17315  mod1ile  17330  mod2ile  17331  latdisdlem  17414  oldmm1  35016  oldmj1  35020  latmrot  35031  latm4  35032  olm01  35035  omllaw4  35045  cmtcomlemN  35047  cmt2N  35049  cmtbr2N  35052  cmtbr3N  35053  cmtbr4N  35054  lecmtN  35055  omlfh1N  35057  omlfh3N  35058  meetat  35095  atnle  35116  atlatmstc  35118  hlrelat2  35202  cvrval5  35214  cvrexchlem  35218  cvrexch  35219  cvrat3  35241  cvrat4  35242  ps-2b  35281  2llnmat  35323  2atm  35326  llnmlplnN  35338  2lplnmN  35358  2llnmj  35359  2llnm2N  35367  2llnm4  35369  2lplnm2N  35420  2lplnmj  35421  dalemcea  35459  dalem16  35478  dalem21  35493  dalem54  35525  dalem55  35526  2lnat  35583  2atm2atN  35584  cdlema1N  35590  hlmod1i  35655  atmod1i1m  35657  atmod2i1  35660  atmod2i2  35661  llnmod2i2  35662  atmod4i1  35665  atmod4i2  35666  llnexchb2lem  35667  dalawlem1  35670  dalawlem2  35671  dalawlem3  35672  dalawlem4  35673  dalawlem5  35674  dalawlem6  35675  dalawlem7  35676  dalawlem8  35677  dalawlem9  35678  dalawlem11  35680  dalawlem12  35681  pmapj2N  35728  psubclinN  35747  poml4N  35752  pl42lem1N  35778  pl42lem2N  35779  pl42N  35782  lhpmcvr3  35824  lhpmcvr4N  35825  lhpmcvr5N  35826  lhpmcvr6N  35827  lhpelim  35836  lhpmod2i2  35837  lhpmod6i1  35838  lhprelat3N  35839  lautm  35893  trlval2  35962  trlcl  35963  trlval3  35986  cdlemc1  35990  cdlemc2  35991  cdlemc4  35993  cdlemc5  35994  cdlemc6  35995  cdlemd2  35998  cdleme0aa  36009  cdleme1b  36025  cdleme1  36026  cdleme2  36027  cdleme3b  36028  cdleme3h  36034  cdleme4a  36038  cdleme5  36039  cdleme7e  36046  cdleme7ga  36047  cdleme9b  36051  cdleme11g  36064  cdleme15d  36076  cdleme15  36077  cdleme16b  36078  cdleme16e  36081  cdleme16f  36082  cdleme22gb  36093  cdlemedb  36096  cdleme20j  36117  cdleme22cN  36141  cdleme22e  36143  cdleme22eALTN  36144  cdleme22f  36145  cdleme23a  36148  cdleme23b  36149  cdleme23c  36150  cdleme28a  36169  cdleme28b  36170  cdleme29ex  36173  cdleme30a  36177  cdlemefr29exN  36201  cdleme32c  36242  cdleme32e  36244  cdleme35b  36249  cdleme35c  36250  cdleme35d  36251  cdleme42c  36271  cdleme42h  36281  cdleme42i  36282  cdleme48bw  36301  cdlemg7fvbwN  36406  cdlemg10bALTN  36435  cdlemg10  36440  cdlemg11b  36441  cdlemg12f  36447  cdlemg12g  36448  cdlemg17a  36460  trlcolem  36525  cdlemkvcl  36641  cdlemk5u  36660  cdlemk37  36713  cdlemk52  36753  dia2dimlem2  36864  docaclN  36923  doca2N  36925  djajN  36936  cdlemn10  37005  dihjustlem  37015  dihord1  37017  dihord2a  37018  dihord2b  37019  dihord2cN  37020  dihord11b  37021  dihord11c  37023  dihord2pre  37024  dihord2pre2  37025  dihlsscpre  37033  dihvalcq2  37046  dihopelvalcpre  37047  dihord6apre  37055  dihord5b  37058  dihord5apre  37061  dihmeetlem1N  37089  dihglblem5apreN  37090  dihglblem2aN  37092  dihglblem2N  37093  dihmeetlem2N  37098  dihglbcpreN  37099  dihmeetbclemN  37103  dihmeetlem3N  37104  dihmeetlem4preN  37105  dihmeetlem6  37108  dihmeetlem7N  37109  dihjatc1  37110  dihjatc2N  37111  dihjatc3  37112  dihmeetlem9N  37114  dihmeetlem16N  37121  dihmeetlem19N  37124  dihmeetcl  37144  dihmeet2  37145  djhlj  37200  dihjatcclem1  37217  dihjatcclem2  37218  dihjatcclem4  37220
  Copyright terms: Public domain W3C validator