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

Theorem latlej1 16883
Description: A join's first argument is less than or equal to the join. (chub1 27750 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 1054 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝐾 ∈ Lat)
5 simp2 1055 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑋𝐵)
6 simp3 1056 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑌𝐵)
7 eqid 2610 . . . 4 (meet‘𝐾) = (meet‘𝐾)
81, 3, 7, 4, 5, 6latcl2 16871 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
98simpld 474 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom )
101, 2, 3, 4, 5, 6, 9lejoin1 16835 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑋 (𝑋 𝑌))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1031   = wceq 1475  wcel 1977  cop 4131   class class class wbr 4583  dom cdm 5038  cfv 5804  (class class class)co 6549  Basecbs 15695  lecple 15775  joincjn 16767  meetcmee 16768  Latclat 16868
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-lub 16797  df-join 16799  df-lat 16869
This theorem is referenced by:  latjlej1  16888  latnlej  16891  latnlej2  16894  latjidm  16897  latnle  16908  latabs2  16911  latmlej11  16913  latjass  16918  mod1ile  16928  lubun  16946  oldmm1  33522  olj01  33530  omllaw5N  33552  cvlexchb1  33635  cvlsupr2  33648  cvlsupr7  33653  hlatlej1  33679  hlrelat5N  33705  2atjm  33749  2llnmj  33864  lplnexllnN  33868  2llnjaN  33870  2llnm2N  33872  4atlem3a  33901  2lplnja  33923  2lplnm2N  33925  2lplnmj  33926  dalemply  33958  dalemsly  33959  dalem10  33977  dalem13  33980  dalem21  33998  dalem55  34031  2llnma1b  34090  cdlema1N  34095  elpaddn0  34104  paddasslem12  34135  paddasslem13  34136  pmapjoin  34156  dalawlem2  34176  dalawlem7  34181  dalawlem11  34185  dalawlem12  34186  lhpmcvr3  34329  lhpmcvr5N  34331  lhpmcvr6N  34332  lautj  34397  trljat1  34471  cdlemc1  34496  cdlemc4  34499  cdleme1  34532  cdleme8  34555  cdleme11g  34570  cdleme22e  34650  cdleme22eALTN  34651  cdleme23b  34656  cdleme23c  34657  cdleme27N  34675  cdleme30a  34684  cdleme35fnpq  34755  cdleme35b  34756  cdleme35c  34757  cdleme42h  34788  cdleme42i  34789  cdleme48bw  34808  cdlemg2fv2  34906  cdlemg7fvbwN  34913  cdlemg8b  34934  cdlemg11b  34948  trlcolem  35032  trljco  35046  cdlemi1  35124  cdlemk48  35256  cdlemn2  35502  dihjustlem  35523  dihord1  35525  dihord5apre  35569  dihglbcpreN  35607  dihmeetlem3N  35612  dihmeetlem11N  35624
  Copyright terms: Public domain W3C validator