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

Theorem latmle2 18423
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 1135 . 2 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ 𝐾 ∈ Lat)
5 simp2 1136 . 2 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ 𝑋 ∈ 𝐡)
6 simp3 1137 . 2 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ π‘Œ ∈ 𝐡)
7 eqid 2731 . . . 4 (joinβ€˜πΎ) = (joinβ€˜πΎ)
81, 7, 3, 4, 5, 6latcl2 18394 . . 3 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ (βŸ¨π‘‹, π‘ŒβŸ© ∈ dom (joinβ€˜πΎ) ∧ βŸ¨π‘‹, π‘ŒβŸ© ∈ dom ∧ ))
98simprd 495 . 2 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ βŸ¨π‘‹, π‘ŒβŸ© ∈ dom ∧ )
101, 2, 3, 4, 5, 6, 9lemeet2 18357 1 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ (𝑋 ∧ π‘Œ) ≀ π‘Œ)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  βŸ¨cop 4634   class class class wbr 5148  dom cdm 5676  β€˜cfv 6543  (class class class)co 7412  Basecbs 17149  lecple 17209  joincjn 18269  meetcmee 18270  Latclat 18389
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7728
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-glb 18305  df-meet 18307  df-lat 18390
This theorem is referenced by:  latmlem1  18427  latledi  18435  mod1ile  18451  oldmm1  38391  olm01  38410  cmtcomlemN  38422  cmtbr4N  38429  meetat  38470  cvrexchlem  38594  cvrat4  38618  2llnmj  38735  2lplnmj  38797  dalem25  38873  dalem54  38901  dalem57  38904  cdlema1N  38966  cdlemb  38969  llnexchb2lem  39043  llnexch2N  39045  dalawlem1  39046  dalawlem3  39048  pl42lem1N  39154  lhpelim  39212  lhpat3  39221  4atexlemunv  39241  4atexlemtlw  39242  4atexlemnclw  39245  4atexlemex2  39246  lautm  39269  trlle  39359  cdlemc2  39367  cdlemc5  39370  cdlemd2  39374  cdleme0b  39387  cdleme0c  39388  cdleme0fN  39393  cdleme01N  39396  cdleme0ex1N  39398  cdleme2  39403  cdleme3b  39404  cdleme3c  39405  cdleme3g  39409  cdleme3h  39410  cdleme7aa  39417  cdleme7c  39420  cdleme7d  39421  cdleme7e  39422  cdleme7ga  39423  cdleme11fN  39439  cdleme11k  39443  cdleme15d  39452  cdleme16f  39458  cdlemednpq  39474  cdleme19c  39480  cdleme20aN  39484  cdleme20c  39486  cdleme20j  39493  cdleme21c  39502  cdleme21ct  39504  cdleme22cN  39517  cdleme22f  39521  cdleme23a  39524  cdleme28a  39545  cdleme35d  39627  cdleme35f  39629  cdlemeg46frv  39700  cdlemeg46rgv  39703  cdlemeg46req  39704  cdlemg2fv2  39775  cdlemg2m  39779  cdlemg4  39792  cdlemg10bALTN  39811  cdlemg31b  39873  trlcolem  39901  cdlemk14  40029  dia2dimlem1  40239  docaclN  40299  doca2N  40301  djajN  40312  dihjustlem  40391  dihord1  40393  dihord2a  40394  dihord2b  40395  dihord2cN  40396  dihord11b  40397  dihord11c  40399  dihord2pre  40400  dihlsscpre  40409  dihvalcq2  40422  dihopelvalcpre  40423  dihord6apre  40431  dihord5b  40434  dihord5apre  40437  dihmeetlem1N  40465  dihglblem5apreN  40466  dihglblem3N  40470  dihmeetbclemN  40479  dihmeetlem4preN  40481  dihmeetlem7N  40485  dihmeetlem9N  40490  dihjatcclem4  40596
  Copyright terms: Public domain W3C validator