MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  latjle12 Structured version   Visualization version   GIF version
Theorem latjle12 18399
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 30749 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 18387 . . 3 (𝐾 ∈ Lat β†’ 𝐾 ∈ Poset)
54adantr 481 . 2 ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝐾 ∈ Poset)
6 simpr1 1194 . 2 ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝑋 ∈ 𝐡)
7 simpr2 1195 . 2 ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ π‘Œ ∈ 𝐡)
8 simpr3 1196 . 2 ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝑍 ∈ 𝐡)
9 eqid 2732 . . . 4 (meetβ€˜πΎ) = (meetβ€˜πΎ)
10 simpl 483 . . . 4 ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝐾 ∈ Lat)
111, 3, 9, 10, 6, 7latcl2 18385 . . 3 ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (βŸ¨π‘‹, π‘ŒβŸ© ∈ dom ∨ ∧ βŸ¨π‘‹, π‘ŒβŸ© ∈ dom (meetβ€˜πΎ)))
1211simpld 495 . 2 ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ βŸ¨π‘‹, π‘ŒβŸ© ∈ dom ∨ )
131, 2, 3, 5, 6, 7, 8, 12joinle 18335 1 ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((𝑋 ≀ 𝑍 ∧ π‘Œ ≀ 𝑍) ↔ (𝑋 ∨ π‘Œ) ≀ 𝑍))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βŸ¨cop 4633   class class class wbr 5147  dom cdm 5675  β€˜cfv 6540  (class class class)co 7405  Basecbs 17140  lecple 17200  Posetcpo 18256  joincjn 18260  meetcmee 18261  Latclat 18380
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-poset 18262  df-lub 18295  df-join 18297  df-lat 18381
This theorem is referenced by:  latleeqj1  18400  latjlej1  18402  latjidm  18411  latledi  18426  latjass  18432  mod1ile  18442  lubun  18464  oldmm1  38075  olj01  38083  cvlexchb1  38188  cvlcvr1  38197  hlrelat  38261  hlrelat2  38262  exatleN  38263  hlrelat3  38271  cvrexchlem  38278  cvratlem  38280  cvrat  38281  atlelt  38297  ps-1  38336  hlatexch3N  38339  hlatexch4  38340  3atlem1  38342  3atlem2  38343  lplnexllnN  38423  2llnjaN  38425  4atlem3  38455  4atlem10  38465  4atlem11b  38467  4atlem11  38468  4atlem12b  38470  4atlem12  38471  2lplnja  38478  dalem1  38518  dalem3  38523  dalem8  38529  dalem16  38538  dalem17  38539  dalem21  38553  dalem25  38557  dalem39  38570  dalem54  38585  dalem60  38591  linepsubN  38611  pmapsub  38627  lneq2at  38637  2llnma3r  38647  cdlema1N  38650  cdlemblem  38652  paddasslem5  38683  paddasslem12  38690  paddasslem13  38691  llnexchb2  38728  dalawlem3  38732  dalawlem5  38734  dalawlem8  38737  dalawlem11  38740  dalawlem12  38741  lhp2lt  38860  lhpexle2lem  38868  lhpexle3lem  38870  4atexlemtlw  38926  4atexlemnclw  38929  lautj  38952  cdlemd3  39059  cdleme3g  39093  cdleme3h  39094  cdleme7d  39105  cdleme11c  39120  cdleme15d  39136  cdleme17b  39146  cdleme19a  39162  cdleme20j  39177  cdleme21c  39186  cdleme22b  39200  cdleme22d  39202  cdleme28a  39229  cdleme35a  39307  cdleme35fnpq  39308  cdleme35b  39309  cdleme35f  39313  cdleme42c  39331  cdleme42i  39342  cdlemf1  39420  cdlemg4c  39471  cdlemg6c  39479  cdlemg8b  39487  cdlemg10  39500  cdlemg11b  39501  cdlemg13a  39510  cdlemg17a  39520  cdlemg18b  39538  cdlemg27a  39551  cdlemg33b0  39560  cdlemg35  39572  cdlemg42  39588  cdlemg46  39594  trljco  39599  tendopltp  39639  cdlemk3  39692  cdlemk10  39702  cdlemk1u  39718  cdlemk39  39775  dialss  39905  dia2dimlem1  39923  dia2dimlem10  39932  dia2dimlem12  39934  cdlemm10N  39977  djajN  39996  diblss  40029  cdlemn2  40054  dihord2pre2  40085  dib2dim  40102  dih2dimb  40103  dih2dimbALTN  40104  dihmeetlem6  40168  dihjatcclem1  40277
  Copyright terms: Public domain W3C validator