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

Theorem latlem12 15248
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 15220 . . 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 995 . 2  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  Y  e.  B )
7 simpr3 996 . 2  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  Z  e.  B )
8 simpr1 994 . 2  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  X  e.  B )
9 eqid 2443 . . . 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 15218 . . 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 15198 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 965    = wceq 1369    e. wcel 1756   <.cop 3883   class class class wbr 4292   dom cdm 4840   ` cfv 5418  (class class class)co 6091   Basecbs 14174   lecple 14245   Posetcpo 15110   joincjn 15114   meetcmee 15115   Latclat 15215
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4403  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-reu 2722  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-iun 4173  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-riota 6052  df-ov 6094  df-oprab 6095  df-poset 15116  df-glb 15145  df-meet 15147  df-lat 15216
This theorem is referenced by:  latleeqm1  15249  latmlem1  15251  latmidm  15256  latledi  15259  mod1ile  15275  oldmm1  32862  olm01  32881  cmtbr4N  32900  atnle  32962  atlatmstc  32964  hlrelat2  33047  cvrval5  33059  cvrexchlem  33063  2atjm  33089  atbtwn  33090  ps-2b  33126  2atm  33171  2llnm4  33214  2llnmeqat  33215  dalemcea  33304  dalem21  33338  dalem54  33370  dalem55  33371  dalem57  33373  2atm2atN  33429  2llnma1b  33430  cdlemblem  33437  dalawlem2  33516  dalawlem3  33517  dalawlem6  33520  dalawlem11  33525  dalawlem12  33526  lhpocnle  33660  lhpmcvr4N  33670  lhpat3  33690  4atexlemcnd  33716  lautm  33738  trlval3  33831  cdlemc5  33839  cdleme3  33881  cdleme7ga  33892  cdleme7  33893  cdleme11k  33912  cdleme16e  33926  cdleme16f  33927  cdlemednpq  33943  cdleme22aa  33983  cdleme22b  33985  cdleme22cN  33986  cdleme23c  33995  cdlemeg46req  34173  cdlemf2  34206  cdlemg10c  34283  cdlemg12f  34292  cdlemg17dALTN  34308  cdlemg19a  34327  cdlemg27b  34340  cdlemi  34464  cdlemk15  34499  cdlemk50  34596  dia2dimlem1  34709  dihopelvalcpre  34893  dihord5b  34904  dihmeetlem1N  34935  dihglblem5apreN  34936  dihglblem2N  34939  dihmeetlem3N  34950
  Copyright terms: Public domain W3C validator