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

Theorem latlem12 15565
Description: An element is less than or equal to a meet iff the element is less than or equal to each argument of the meet. (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
latlem12  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .<_  Y  /\  X  .<_  Z )  <->  X  .<_  ( Y  ./\  Z )
) )

Proof of Theorem latlem12
StepHypRef Expression
1 latmle.b . 2  |-  B  =  ( Base `  K
)
2 latmle.l . 2  |-  .<_  =  ( le `  K )
3 latmle.m . 2  |-  ./\  =  ( meet `  K )
4 latpos 15537 . . 3  |-  ( K  e.  Lat  ->  K  e.  Poset )
54adantr 465 . 2  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  K  e.  Poset )
6 simpr2 1003 . 2  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  Y  e.  B )
7 simpr3 1004 . 2  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  Z  e.  B )
8 simpr1 1002 . 2  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  X  e.  B )
9 eqid 2467 . . . 4  |-  ( join `  K )  =  (
join `  K )
10 simpl 457 . . . 4  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  K  e.  Lat )
111, 9, 3, 10, 6, 7latcl2 15535 . . 3  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( <. Y ,  Z >.  e. 
dom  ( join `  K
)  /\  <. Y ,  Z >.  e.  dom  ./\  )
)
1211simprd 463 . 2  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  <. Y ,  Z >.  e.  dom  ./\  )
131, 2, 3, 5, 6, 7, 8, 12meetle 15515 1  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .<_  Y  /\  X  .<_  Z )  <->  X  .<_  ( Y  ./\  Z )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 973    = wceq 1379    e. wcel 1767   <.cop 4033   class class class wbr 4447   dom cdm 4999   ` cfv 5588  (class class class)co 6284   Basecbs 14490   lecple 14562   Posetcpo 15427   joincjn 15431   meetcmee 15432   Latclat 15532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-riota 6245  df-ov 6287  df-oprab 6288  df-poset 15433  df-glb 15462  df-meet 15464  df-lat 15533
This theorem is referenced by:  latleeqm1  15566  latmlem1  15568  latmidm  15573  latledi  15576  mod1ile  15592  oldmm1  34032  olm01  34051  cmtbr4N  34070  atnle  34132  atlatmstc  34134  hlrelat2  34217  cvrval5  34229  cvrexchlem  34233  2atjm  34259  atbtwn  34260  ps-2b  34296  2atm  34341  2llnm4  34384  2llnmeqat  34385  dalemcea  34474  dalem21  34508  dalem54  34540  dalem55  34541  dalem57  34543  2atm2atN  34599  2llnma1b  34600  cdlemblem  34607  dalawlem2  34686  dalawlem3  34687  dalawlem6  34690  dalawlem11  34695  dalawlem12  34696  lhpocnle  34830  lhpmcvr4N  34840  lhpat3  34860  4atexlemcnd  34886  lautm  34908  trlval3  35001  cdlemc5  35009  cdleme3  35051  cdleme7ga  35062  cdleme7  35063  cdleme11k  35082  cdleme16e  35096  cdleme16f  35097  cdlemednpq  35113  cdleme22aa  35153  cdleme22b  35155  cdleme22cN  35156  cdleme23c  35165  cdlemeg46req  35343  cdlemf2  35376  cdlemg10c  35453  cdlemg12f  35462  cdlemg17dALTN  35478  cdlemg19a  35497  cdlemg27b  35510  cdlemi  35634  cdlemk15  35669  cdlemk50  35766  dia2dimlem1  35879  dihopelvalcpre  36063  dihord5b  36074  dihmeetlem1N  36105  dihglblem5apreN  36106  dihglblem2N  36109  dihmeetlem3N  36120
  Copyright terms: Public domain W3C validator