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

Theorem latmle2 16900
Description: A meet is less than or equal to its second argument. (Contributed by NM, 21-Oct-2011.)
Hypotheses
Ref Expression
latmle.b 𝐵 = (Base‘𝐾)
latmle.l = (le‘𝐾)
latmle.m = (meet‘𝐾)
Assertion
Ref Expression
latmle2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) 𝑌)

Proof of Theorem latmle2
StepHypRef Expression
1 latmle.b . 2 𝐵 = (Base‘𝐾)
2 latmle.l . 2 = (le‘𝐾)
3 latmle.m . 2 = (meet‘𝐾)
4 simp1 1054 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝐾 ∈ Lat)
5 simp2 1055 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑋𝐵)
6 simp3 1056 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑌𝐵)
7 eqid 2610 . . . 4 (join‘𝐾) = (join‘𝐾)
81, 7, 3, 4, 5, 6latcl2 16871 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom (join‘𝐾) ∧ ⟨𝑋, 𝑌⟩ ∈ dom ))
98simprd 478 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom )
101, 2, 3, 4, 5, 6, 9lemeet2 16850 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) 𝑌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1031   = wceq 1475  wcel 1977  cop 4131   class class class wbr 4583  dom cdm 5038  cfv 5804  (class class class)co 6549  Basecbs 15695  lecple 15775  joincjn 16767  meetcmee 16768  Latclat 16868
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-glb 16798  df-meet 16800  df-lat 16869
This theorem is referenced by:  latmlem1  16904  latledi  16912  mod1ile  16928  oldmm1  33522  olm01  33541  cmtcomlemN  33553  cmtbr4N  33560  meetat  33601  cvrexchlem  33723  cvrat4  33747  2llnmj  33864  2lplnmj  33926  dalem25  34002  dalem54  34030  dalem57  34033  cdlema1N  34095  cdlemb  34098  llnexchb2lem  34172  llnexch2N  34174  dalawlem1  34175  dalawlem3  34177  pl42lem1N  34283  lhpelim  34341  lhpat3  34350  4atexlemunv  34370  4atexlemtlw  34371  4atexlemnclw  34374  4atexlemex2  34375  lautm  34398  trlle  34489  cdlemc2  34497  cdlemc5  34500  cdlemd2  34504  cdleme0b  34517  cdleme0c  34518  cdleme0fN  34523  cdleme01N  34526  cdleme0ex1N  34528  cdleme2  34533  cdleme3b  34534  cdleme3c  34535  cdleme3g  34539  cdleme3h  34540  cdleme7aa  34547  cdleme7c  34550  cdleme7d  34551  cdleme7e  34552  cdleme7ga  34553  cdleme11fN  34569  cdleme11k  34573  cdleme15d  34582  cdleme16f  34588  cdlemednpq  34604  cdleme19c  34611  cdleme20aN  34615  cdleme20c  34617  cdleme20j  34624  cdleme21c  34633  cdleme21ct  34635  cdleme22cN  34648  cdleme22f  34652  cdleme23a  34655  cdleme28a  34676  cdleme35d  34758  cdleme35f  34760  cdlemeg46frv  34831  cdlemeg46rgv  34834  cdlemeg46req  34835  cdlemg2fv2  34906  cdlemg2m  34910  cdlemg4  34923  cdlemg10bALTN  34942  cdlemg31b  35004  trlcolem  35032  cdlemk14  35160  dia2dimlem1  35371  docaclN  35431  doca2N  35433  djajN  35444  dihjustlem  35523  dihord1  35525  dihord2a  35526  dihord2b  35527  dihord2cN  35528  dihord11b  35529  dihord11c  35531  dihord2pre  35532  dihlsscpre  35541  dihvalcq2  35554  dihopelvalcpre  35555  dihord6apre  35563  dihord5b  35566  dihord5apre  35569  dihmeetlem1N  35597  dihglblem5apreN  35598  dihglblem3N  35602  dihmeetbclemN  35611  dihmeetlem4preN  35613  dihmeetlem7N  35617  dihmeetlem9N  35622  dihjatcclem4  35728
  Copyright terms: Public domain W3C validator