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

Theorem latlej1 18403
Description: A join's first argument is less than or equal to the join. (chub1 30798 analog.) (Contributed by NM, 17-Sep-2011.)
Hypotheses
Ref Expression
latlej.b 𝐡 = (Baseβ€˜πΎ)
latlej.l ≀ = (leβ€˜πΎ)
latlej.j ∨ = (joinβ€˜πΎ)
Assertion
Ref Expression
latlej1 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ 𝑋 ≀ (𝑋 ∨ π‘Œ))

Proof of Theorem latlej1
StepHypRef Expression
1 latlej.b . 2 𝐡 = (Baseβ€˜πΎ)
2 latlej.l . 2 ≀ = (leβ€˜πΎ)
3 latlej.j . 2 ∨ = (joinβ€˜πΎ)
4 simp1 1136 . 2 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ 𝐾 ∈ Lat)
5 simp2 1137 . 2 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ 𝑋 ∈ 𝐡)
6 simp3 1138 . 2 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ π‘Œ ∈ 𝐡)
7 eqid 2732 . . . 4 (meetβ€˜πΎ) = (meetβ€˜πΎ)
81, 3, 7, 4, 5, 6latcl2 18391 . . 3 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ (βŸ¨π‘‹, π‘ŒβŸ© ∈ dom ∨ ∧ βŸ¨π‘‹, π‘ŒβŸ© ∈ dom (meetβ€˜πΎ)))
98simpld 495 . 2 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ βŸ¨π‘‹, π‘ŒβŸ© ∈ dom ∨ )
101, 2, 3, 4, 5, 6, 9lejoin1 18339 1 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ 𝑋 ≀ (𝑋 ∨ π‘Œ))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βŸ¨cop 4634   class class class wbr 5148  dom cdm 5676  β€˜cfv 6543  (class class class)co 7411  Basecbs 17146  lecple 17206  joincjn 18266  meetcmee 18267  Latclat 18386
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 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
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 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-lub 18301  df-join 18303  df-lat 18387
This theorem is referenced by:  latjlej1  18408  latnlej  18411  latnlej2  18414  latjidm  18417  latnle  18428  latabs2  18431  latmlej11  18433  latjass  18438  mod1ile  18448  lubun  18470  oldmm1  38173  olj01  38181  omllaw5N  38203  cvlexchb1  38286  cvlsupr2  38299  cvlsupr7  38304  hlatlej1  38331  hlrelat5N  38358  2atjm  38402  2llnmj  38517  lplnexllnN  38521  2llnjaN  38523  2llnm2N  38525  4atlem3a  38554  2lplnja  38576  2lplnm2N  38578  2lplnmj  38579  dalemply  38611  dalemsly  38612  dalem10  38630  dalem13  38633  dalem21  38651  dalem55  38684  2llnma1b  38743  cdlema1N  38748  elpaddn0  38757  paddasslem12  38788  paddasslem13  38789  pmapjoin  38809  dalawlem2  38829  dalawlem7  38834  dalawlem11  38838  dalawlem12  38839  lhpmcvr3  38982  lhpmcvr5N  38984  lhpmcvr6N  38985  lautj  39050  trljat1  39123  cdlemc1  39148  cdlemc4  39151  cdleme1  39184  cdleme8  39207  cdleme11g  39222  cdleme22e  39301  cdleme22eALTN  39302  cdleme23b  39307  cdleme23c  39308  cdleme27N  39326  cdleme30a  39335  cdleme35fnpq  39406  cdleme35b  39407  cdleme35c  39408  cdleme42h  39439  cdleme42i  39440  cdleme48bw  39459  cdlemg2fv2  39557  cdlemg7fvbwN  39564  cdlemg8b  39585  cdlemg11b  39599  trlcolem  39683  trljco  39697  cdlemi1  39775  cdlemk48  39907  cdlemn2  40152  dihjustlem  40173  dihord1  40175  dihord5apre  40219  dihglbcpreN  40257  dihmeetlem3N  40262  dihmeetlem11N  40274
  Copyright terms: Public domain W3C validator