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

Theorem latjle12 17667
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 29295 analog.) (Contributed by NM, 17-Sep-2011.)
Hypotheses
Ref Expression
latlej.b 𝐵 = (Base‘𝐾)
latlej.l = (le‘𝐾)
latlej.j = (join‘𝐾)
Assertion
Ref Expression
latjle12 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑍𝑌 𝑍) ↔ (𝑋 𝑌) 𝑍))

Proof of Theorem latjle12
StepHypRef Expression
1 latlej.b . 2 𝐵 = (Base‘𝐾)
2 latlej.l . 2 = (le‘𝐾)
3 latlej.j . 2 = (join‘𝐾)
4 latpos 17655 . . 3 (𝐾 ∈ Lat → 𝐾 ∈ Poset)
54adantr 484 . 2 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝐾 ∈ Poset)
6 simpr1 1191 . 2 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝑋𝐵)
7 simpr2 1192 . 2 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝑌𝐵)
8 simpr3 1193 . 2 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝑍𝐵)
9 eqid 2801 . . . 4 (meet‘𝐾) = (meet‘𝐾)
10 simpl 486 . . . 4 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → 𝐾 ∈ Lat)
111, 3, 9, 10, 6, 7latcl2 17653 . . 3 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (⟨𝑋, 𝑌⟩ ∈ dom ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
1211simpld 498 . 2 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ⟨𝑋, 𝑌⟩ ∈ dom )
131, 2, 3, 5, 6, 7, 8, 12joinle 17619 1 ((𝐾 ∈ Lat ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑍𝑌 𝑍) ↔ (𝑋 𝑌) 𝑍))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2112  cop 4534   class class class wbr 5033  dom cdm 5523  cfv 6328  (class class class)co 7139  Basecbs 16478  lecple 16567  Posetcpo 17545  joincjn 17549  meetcmee 17550  Latclat 17650
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-poset 17551  df-lub 17579  df-join 17581  df-lat 17651
This theorem is referenced by:  latleeqj1  17668  latjlej1  17670  latjidm  17679  latledi  17694  latjass  17700  mod1ile  17710  lubun  17728  oldmm1  36506  olj01  36514  cvlexchb1  36619  cvlcvr1  36628  hlrelat  36691  hlrelat2  36692  exatleN  36693  hlrelat3  36701  cvrexchlem  36708  cvratlem  36710  cvrat  36711  atlelt  36727  ps-1  36766  hlatexch3N  36769  hlatexch4  36770  3atlem1  36772  3atlem2  36773  lplnexllnN  36853  2llnjaN  36855  4atlem3  36885  4atlem10  36895  4atlem11b  36897  4atlem11  36898  4atlem12b  36900  4atlem12  36901  2lplnja  36908  dalem1  36948  dalem3  36953  dalem8  36959  dalem16  36968  dalem17  36969  dalem21  36983  dalem25  36987  dalem39  37000  dalem54  37015  dalem60  37021  linepsubN  37041  pmapsub  37057  lneq2at  37067  2llnma3r  37077  cdlema1N  37080  cdlemblem  37082  paddasslem5  37113  paddasslem12  37120  paddasslem13  37121  llnexchb2  37158  dalawlem3  37162  dalawlem5  37164  dalawlem8  37167  dalawlem11  37170  dalawlem12  37171  lhp2lt  37290  lhpexle2lem  37298  lhpexle3lem  37300  4atexlemtlw  37356  4atexlemnclw  37359  lautj  37382  cdlemd3  37489  cdleme3g  37523  cdleme3h  37524  cdleme7d  37535  cdleme11c  37550  cdleme15d  37566  cdleme17b  37576  cdleme19a  37592  cdleme20j  37607  cdleme21c  37616  cdleme22b  37630  cdleme22d  37632  cdleme28a  37659  cdleme35a  37737  cdleme35fnpq  37738  cdleme35b  37739  cdleme35f  37743  cdleme42c  37761  cdleme42i  37772  cdlemf1  37850  cdlemg4c  37901  cdlemg6c  37909  cdlemg8b  37917  cdlemg10  37930  cdlemg11b  37931  cdlemg13a  37940  cdlemg17a  37950  cdlemg18b  37968  cdlemg27a  37981  cdlemg33b0  37990  cdlemg35  38002  cdlemg42  38018  cdlemg46  38024  trljco  38029  tendopltp  38069  cdlemk3  38122  cdlemk10  38132  cdlemk1u  38148  cdlemk39  38205  dialss  38335  dia2dimlem1  38353  dia2dimlem10  38362  dia2dimlem12  38364  cdlemm10N  38407  djajN  38426  diblss  38459  cdlemn2  38484  dihord2pre2  38515  dib2dim  38532  dih2dimb  38533  dih2dimbALTN  38534  dihmeetlem6  38598  dihjatcclem1  38707
  Copyright terms: Public domain W3C validator