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

Theorem latlem12 15244
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 15216 . . 3  |-  ( K  e.  Lat  ->  K  e.  Poset )
54adantr 462 . 2  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  K  e.  Poset )
6 simpr2 990 . 2  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  Y  e.  B )
7 simpr3 991 . 2  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  Z  e.  B )
8 simpr1 989 . 2  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  X  e.  B )
9 eqid 2441 . . . 4  |-  ( join `  K )  =  (
join `  K )
10 simpl 454 . . . 4  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  K  e.  Lat )
111, 9, 3, 10, 6, 7latcl2 15214 . . 3  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( <. Y ,  Z >.  e. 
dom  ( join `  K
)  /\  <. Y ,  Z >.  e.  dom  ./\  )
)
1211simprd 460 . 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 15194 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 960    = wceq 1364    e. wcel 1761   <.cop 3880   class class class wbr 4289   dom cdm 4836   ` cfv 5415  (class class class)co 6090   Basecbs 14170   lecple 14241   Posetcpo 15106   joincjn 15110   meetcmee 15111   Latclat 15211
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-riota 6049  df-ov 6093  df-oprab 6094  df-poset 15112  df-glb 15141  df-meet 15143  df-lat 15212
This theorem is referenced by:  latleeqm1  15245  latmlem1  15247  latmidm  15252  latledi  15255  mod1ile  15271  oldmm1  32550  olm01  32569  cmtbr4N  32588  atnle  32650  atlatmstc  32652  hlrelat2  32735  cvrval5  32747  cvrexchlem  32751  2atjm  32777  atbtwn  32778  ps-2b  32814  2atm  32859  2llnm4  32902  2llnmeqat  32903  dalemcea  32992  dalem21  33026  dalem54  33058  dalem55  33059  dalem57  33061  2atm2atN  33117  2llnma1b  33118  cdlemblem  33125  dalawlem2  33204  dalawlem3  33205  dalawlem6  33208  dalawlem11  33213  dalawlem12  33214  lhpocnle  33348  lhpmcvr4N  33358  lhpat3  33378  4atexlemcnd  33404  lautm  33426  trlval3  33519  cdlemc5  33527  cdleme3  33569  cdleme7ga  33580  cdleme7  33581  cdleme11k  33600  cdleme16e  33614  cdleme16f  33615  cdlemednpq  33631  cdleme22aa  33671  cdleme22b  33673  cdleme22cN  33674  cdleme23c  33683  cdlemeg46req  33861  cdlemf2  33894  cdlemg10c  33971  cdlemg12f  33980  cdlemg17dALTN  33996  cdlemg19a  34015  cdlemg27b  34028  cdlemi  34152  cdlemk15  34187  cdlemk50  34284  dia2dimlem1  34397  dihopelvalcpre  34581  dihord5b  34592  dihmeetlem1N  34623  dihglblem5apreN  34624  dihglblem2N  34627  dihmeetlem3N  34638
  Copyright terms: Public domain W3C validator