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

Theorem latmle2 14465
Description: A meet is less than or equal to its second argument. (inss2 3526 analog.) (Contributed by NM, 21-Oct-2011.)
Hypotheses
Ref Expression
latmle.b  |-  B  =  ( Base `  K
)
latmle.l  |-  .<_  =  ( le `  K )
latmle.m  |-  ./\  =  ( meet `  K )
Assertion
Ref Expression
latmle2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  ./\  Y
)  .<_  Y )

Proof of Theorem latmle2
StepHypRef Expression
1 latmle.b . . 3  |-  B  =  ( Base `  K
)
2 latmle.m . . 3  |-  ./\  =  ( meet `  K )
31, 2latmcl 14439 . 2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  ./\  Y
)  e.  B )
4 latmle.l . . 3  |-  .<_  =  ( le `  K )
51, 4, 2lemeet2 14415 . 2  |-  ( ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  /\  ( X  ./\  Y
)  e.  B )  ->  ( X  ./\  Y )  .<_  Y )
63, 5mpdan 650 1  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  ./\  Y
)  .<_  Y )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936    = wceq 1649    e. wcel 1721   class class class wbr 4176   ` cfv 5417  (class class class)co 6044   Basecbs 13428   lecple 13495   meetcmee 14361   Latclat 14433
This theorem is referenced by:  latmlem1  14469  latledi  14477  mod1ile  14493  oldmm1  29704  olm01  29723  cmtcomlemN  29735  cmtbr4N  29742  meetat  29783  cvrexchlem  29905  cvrat4  29929  2llnmj  30046  2lplnmj  30108  dalem25  30184  dalem54  30212  dalem57  30215  cdlema1N  30277  cdlemb  30280  llnexchb2lem  30354  llnexch2N  30356  dalawlem1  30357  dalawlem3  30359  pl42lem1N  30465  lhpelim  30523  lhpat3  30532  4atexlemunv  30552  4atexlemtlw  30553  4atexlemnclw  30556  4atexlemex2  30557  lautm  30580  trlle  30670  cdlemc2  30678  cdlemc5  30681  cdlemd2  30685  cdleme0b  30698  cdleme0c  30699  cdleme0fN  30704  cdleme01N  30707  cdleme0ex1N  30709  cdleme2  30714  cdleme3b  30715  cdleme3c  30716  cdleme3g  30720  cdleme3h  30721  cdleme7aa  30728  cdleme7c  30731  cdleme7d  30732  cdleme7e  30733  cdleme7ga  30734  cdleme11fN  30750  cdleme11k  30754  cdleme15d  30763  cdleme16f  30769  cdlemednpq  30785  cdleme19c  30791  cdleme20aN  30795  cdleme20c  30797  cdleme20j  30804  cdleme21c  30813  cdleme21ct  30815  cdleme22cN  30828  cdleme22f  30832  cdleme23a  30835  cdleme28a  30856  cdleme35d  30938  cdleme35f  30940  cdlemeg46frv  31011  cdlemeg46rgv  31014  cdlemeg46req  31015  cdlemg2fv2  31086  cdlemg2m  31090  cdlemg4  31103  cdlemg10bALTN  31122  cdlemg31b  31184  trlcolem  31212  cdlemk14  31340  dia2dimlem1  31551  docaclN  31611  doca2N  31613  djajN  31624  dihjustlem  31703  dihord1  31705  dihord2a  31706  dihord2b  31707  dihord2cN  31708  dihord11b  31709  dihord11c  31711  dihord2pre  31712  dihlsscpre  31721  dihvalcq2  31734  dihopelvalcpre  31735  dihord6apre  31743  dihord5b  31746  dihord5apre  31749  dihmeetlem1N  31777  dihglblem5apreN  31778  dihglblem3N  31782  dihmeetbclemN  31791  dihmeetlem4preN  31793  dihmeetlem7N  31797  dihmeetlem9N  31802  dihjatcclem4  31908
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-rep 4284  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-nel 2574  df-ral 2675  df-rex 2676  df-reu 2677  df-rab 2679  df-v 2922  df-sbc 3126  df-csb 3216  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-iun 4059  df-br 4177  df-opab 4231  df-mpt 4232  df-id 4462  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-res 4853  df-ima 4854  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-ov 6047  df-oprab 6048  df-mpt2 6049  df-1st 6312  df-2nd 6313  df-undef 6506  df-riota 6512  df-glb 14391  df-meet 14393  df-lat 14434
  Copyright terms: Public domain W3C validator