MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  latjle12 Structured version   Visualization version   GIF version
Theorem latjle12 18451
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 31347 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 18439 . . 3 (𝐾 ∈ Lat β†’ 𝐾 ∈ Poset)
54adantr 479 . 2 ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝐾 ∈ Poset)
6 simpr1 1191 . 2 ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝑋 ∈ 𝐡)
7 simpr2 1192 . 2 ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ π‘Œ ∈ 𝐡)
8 simpr3 1193 . 2 ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝑍 ∈ 𝐡)
9 eqid 2728 . . . 4 (meetβ€˜πΎ) = (meetβ€˜πΎ)
10 simpl 481 . . . 4 ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ 𝐾 ∈ Lat)
111, 3, 9, 10, 6, 7latcl2 18437 . . 3 ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ (βŸ¨π‘‹, π‘ŒβŸ© ∈ dom ∨ ∧ βŸ¨π‘‹, π‘ŒβŸ© ∈ dom (meetβ€˜πΎ)))
1211simpld 493 . 2 ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ βŸ¨π‘‹, π‘ŒβŸ© ∈ dom ∨ )
131, 2, 3, 5, 6, 7, 8, 12joinle 18387 1 ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡 ∧ 𝑍 ∈ 𝐡)) β†’ ((𝑋 ≀ 𝑍 ∧ π‘Œ ≀ 𝑍) ↔ (𝑋 ∨ π‘Œ) ≀ 𝑍))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  βŸ¨cop 4638   class class class wbr 5152  dom cdm 5682  β€˜cfv 6553  (class class class)co 7426  Basecbs 17189  lecple 17249  Posetcpo 18308  joincjn 18312  meetcmee 18313  Latclat 18432
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7748
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-poset 18314  df-lub 18347  df-join 18349  df-lat 18433
This theorem is referenced by:  latleeqj1  18452  latjlej1  18454  latjidm  18463  latledi  18478  latjass  18484  mod1ile  18494  lubun  18516  oldmm1  38729  olj01  38737  cvlexchb1  38842  cvlcvr1  38851  hlrelat  38915  hlrelat2  38916  exatleN  38917  hlrelat3  38925  cvrexchlem  38932  cvratlem  38934  cvrat  38935  atlelt  38951  ps-1  38990  hlatexch3N  38993  hlatexch4  38994  3atlem1  38996  3atlem2  38997  lplnexllnN  39077  2llnjaN  39079  4atlem3  39109  4atlem10  39119  4atlem11b  39121  4atlem11  39122  4atlem12b  39124  4atlem12  39125  2lplnja  39132  dalem1  39172  dalem3  39177  dalem8  39183  dalem16  39192  dalem17  39193  dalem21  39207  dalem25  39211  dalem39  39224  dalem54  39239  dalem60  39245  linepsubN  39265  pmapsub  39281  lneq2at  39291  2llnma3r  39301  cdlema1N  39304  cdlemblem  39306  paddasslem5  39337  paddasslem12  39344  paddasslem13  39345  llnexchb2  39382  dalawlem3  39386  dalawlem5  39388  dalawlem8  39391  dalawlem11  39394  dalawlem12  39395  lhp2lt  39514  lhpexle2lem  39522  lhpexle3lem  39524  4atexlemtlw  39580  4atexlemnclw  39583  lautj  39606  cdlemd3  39713  cdleme3g  39747  cdleme3h  39748  cdleme7d  39759  cdleme11c  39774  cdleme15d  39790  cdleme17b  39800  cdleme19a  39816  cdleme20j  39831  cdleme21c  39840  cdleme22b  39854  cdleme22d  39856  cdleme28a  39883  cdleme35a  39961  cdleme35fnpq  39962  cdleme35b  39963  cdleme35f  39967  cdleme42c  39985  cdleme42i  39996  cdlemf1  40074  cdlemg4c  40125  cdlemg6c  40133  cdlemg8b  40141  cdlemg10  40154  cdlemg11b  40155  cdlemg13a  40164  cdlemg17a  40174  cdlemg18b  40192  cdlemg27a  40205  cdlemg33b0  40214  cdlemg35  40226  cdlemg42  40242  cdlemg46  40248  trljco  40253  tendopltp  40293  cdlemk3  40346  cdlemk10  40356  cdlemk1u  40372  cdlemk39  40429  dialss  40559  dia2dimlem1  40577  dia2dimlem10  40586  dia2dimlem12  40588  cdlemm10N  40631  djajN  40650  diblss  40683  cdlemn2  40708  dihord2pre2  40739  dib2dim  40756  dih2dimb  40757  dih2dimbALTN  40758  dihmeetlem6  40822  dihjatcclem1  40931
  Copyright terms: Public domain W3C validator