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

Theorem latjle12 14170
Description: A join is less than or equal to a third value iff each argument is less than or equal to the third value. (chlub 22090 analog.) (Contributed by NM, 17-Sep-2011.)
Hypotheses
Ref Expression
latlej.b  |-  B  =  ( Base `  K
)
latlej.l  |-  .<_  =  ( le `  K )
latlej.j  |-  .\/  =  ( join `  K )
Assertion
Ref Expression
latjle12  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .<_  Z  /\  Y  .<_  Z )  <->  ( X  .\/  Y )  .<_  Z ) )

Proof of Theorem latjle12
StepHypRef Expression
1 latlej.b . . . 4  |-  B  =  ( Base `  K
)
2 latlej.j . . . 4  |-  .\/  =  ( join `  K )
31, 2latjcl 14158 . . 3  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( X  .\/  Y
)  e.  B )
433adant3r3 1162 . 2  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  ( X  .\/  Y )  e.  B )
5 latpos 14157 . . 3  |-  ( K  e.  Lat  ->  K  e.  Poset )
6 latlej.l . . . 4  |-  .<_  =  ( le `  K )
71, 6, 2joinle 14129 . . 3  |-  ( ( K  e.  Poset  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B )  /\  ( X  .\/  Y
)  e.  B )  ->  ( ( X 
.<_  Z  /\  Y  .<_  Z )  <->  ( X  .\/  Y )  .<_  Z )
)
85, 7syl3an1 1215 . 2  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
)  /\  ( X  .\/  Y )  e.  B
)  ->  ( ( X  .<_  Z  /\  Y  .<_  Z )  <->  ( X  .\/  Y )  .<_  Z ) )
94, 8mpd3an3 1278 1  |-  ( ( K  e.  Lat  /\  ( X  e.  B  /\  Y  e.  B  /\  Z  e.  B
) )  ->  (
( X  .<_  Z  /\  Y  .<_  Z )  <->  ( X  .\/  Y )  .<_  Z ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1625    e. wcel 1686   class class class wbr 4025   ` cfv 5257  (class class class)co 5860   Basecbs 13150   lecple 13217   Posetcpo 14076   joincjn 14080   Latclat 14153
This theorem is referenced by:  latleeqj1  14171  latjlej1  14173  latjidm  14182  latledi  14197  latjass  14203  mod1ile  14213  lubun  14229  lubunNEW  29236  oldmm1  29480  olj01  29488  cvlexchb1  29593  cvlcvr1  29602  hlrelat  29664  hlrelat2  29665  exatleN  29666  hlrelat3  29674  cvrexchlem  29681  cvratlem  29683  cvrat  29684  atlelt  29700  ps-1  29739  hlatexch3N  29742  hlatexch4  29743  3atlem1  29745  3atlem2  29746  lplnexllnN  29826  2llnjaN  29828  4atlem3  29858  4atlem10  29868  4atlem11b  29870  4atlem11  29871  4atlem12b  29873  4atlem12  29874  2lplnja  29881  dalem1  29921  dalem3  29926  dalem8  29932  dalem16  29941  dalem17  29942  dalem21  29956  dalem25  29960  dalem39  29973  dalem54  29988  dalem60  29994  linepsubN  30014  pmapsub  30030  lneq2at  30040  2llnma3r  30050  cdlema1N  30053  cdlemblem  30055  paddasslem5  30086  paddasslem12  30093  paddasslem13  30094  llnexchb2  30131  dalawlem3  30135  dalawlem5  30137  dalawlem8  30140  dalawlem11  30143  dalawlem12  30144  lhp2lt  30263  lhpexle2lem  30271  lhpexle3lem  30273  4atexlemtlw  30329  4atexlemnclw  30332  lautj  30355  cdlemd3  30462  cdleme3g  30496  cdleme3h  30497  cdleme7d  30508  cdleme11c  30523  cdleme15d  30539  cdleme17b  30549  cdleme19a  30565  cdleme20j  30580  cdleme21c  30589  cdleme22b  30603  cdleme22d  30605  cdleme28a  30632  cdleme35a  30710  cdleme35fnpq  30711  cdleme35b  30712  cdleme35f  30716  cdleme42c  30734  cdleme42i  30745  cdlemf1  30823  cdlemg4c  30874  cdlemg6c  30882  cdlemg8b  30890  cdlemg10  30903  cdlemg11b  30904  cdlemg13a  30913  cdlemg17a  30923  cdlemg18b  30941  cdlemg27a  30954  cdlemg33b0  30963  cdlemg35  30975  cdlemg42  30991  cdlemg46  30997  trljco  31002  tendopltp  31042  cdlemk3  31095  cdlemk10  31105  cdlemk1u  31121  cdlemk39  31178  dialss  31309  dia2dimlem1  31327  dia2dimlem10  31336  dia2dimlem12  31338  cdlemm10N  31381  djajN  31400  diblss  31433  cdlemn2  31458  dihord2pre2  31489  dib2dim  31506  dih2dimb  31507  dih2dimbALTN  31508  dihmeetlem6  31572  dihjatcclem1  31681
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-rep 4133  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-nel 2451  df-ral 2550  df-rex 2551  df-reu 2552  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-iun 3909  df-br 4026  df-opab 4080  df-mpt 4081  df-id 4311  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-ov 5863  df-oprab 5864  df-mpt2 5865  df-1st 6124  df-2nd 6125  df-undef 6300  df-riota 6306  df-poset 14082  df-lub 14110  df-join 14112  df-lat 14154
  Copyright terms: Public domain W3C validator