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

Theorem latmle2 16998
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 1059 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝐾 ∈ Lat)
5 simp2 1060 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑋𝐵)
6 simp3 1061 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑌𝐵)
7 eqid 2621 . . . 4 (join‘𝐾) = (join‘𝐾)
81, 7, 3, 4, 5, 6latcl2 16969 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom (join‘𝐾) ∧ ⟨𝑋, 𝑌⟩ ∈ dom ))
98simprd 479 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom )
101, 2, 3, 4, 5, 6, 9lemeet2 16948 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) 𝑌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036   = wceq 1480  wcel 1987  cop 4154   class class class wbr 4613  dom cdm 5074  cfv 5847  (class class class)co 6604  Basecbs 15781  lecple 15869  joincjn 16865  meetcmee 16866  Latclat 16966
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-glb 16896  df-meet 16898  df-lat 16967
This theorem is referenced by:  latmlem1  17002  latledi  17010  mod1ile  17026  oldmm1  33984  olm01  34003  cmtcomlemN  34015  cmtbr4N  34022  meetat  34063  cvrexchlem  34185  cvrat4  34209  2llnmj  34326  2lplnmj  34388  dalem25  34464  dalem54  34492  dalem57  34495  cdlema1N  34557  cdlemb  34560  llnexchb2lem  34634  llnexch2N  34636  dalawlem1  34637  dalawlem3  34639  pl42lem1N  34745  lhpelim  34803  lhpat3  34812  4atexlemunv  34832  4atexlemtlw  34833  4atexlemnclw  34836  4atexlemex2  34837  lautm  34860  trlle  34951  cdlemc2  34959  cdlemc5  34962  cdlemd2  34966  cdleme0b  34979  cdleme0c  34980  cdleme0fN  34985  cdleme01N  34988  cdleme0ex1N  34990  cdleme2  34995  cdleme3b  34996  cdleme3c  34997  cdleme3g  35001  cdleme3h  35002  cdleme7aa  35009  cdleme7c  35012  cdleme7d  35013  cdleme7e  35014  cdleme7ga  35015  cdleme11fN  35031  cdleme11k  35035  cdleme15d  35044  cdleme16f  35050  cdlemednpq  35066  cdleme19c  35073  cdleme20aN  35077  cdleme20c  35079  cdleme20j  35086  cdleme21c  35095  cdleme21ct  35097  cdleme22cN  35110  cdleme22f  35114  cdleme23a  35117  cdleme28a  35138  cdleme35d  35220  cdleme35f  35222  cdlemeg46frv  35293  cdlemeg46rgv  35296  cdlemeg46req  35297  cdlemg2fv2  35368  cdlemg2m  35372  cdlemg4  35385  cdlemg10bALTN  35404  cdlemg31b  35466  trlcolem  35494  cdlemk14  35622  dia2dimlem1  35833  docaclN  35893  doca2N  35895  djajN  35906  dihjustlem  35985  dihord1  35987  dihord2a  35988  dihord2b  35989  dihord2cN  35990  dihord11b  35991  dihord11c  35993  dihord2pre  35994  dihlsscpre  36003  dihvalcq2  36016  dihopelvalcpre  36017  dihord6apre  36025  dihord5b  36028  dihord5apre  36031  dihmeetlem1N  36059  dihglblem5apreN  36060  dihglblem3N  36064  dihmeetbclemN  36073  dihmeetlem4preN  36075  dihmeetlem7N  36079  dihmeetlem9N  36084  dihjatcclem4  36190
  Copyright terms: Public domain W3C validator