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

Theorem latlej1 18297
Description: A join's first argument is less than or equal to the join. (chub1 30278 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 1137 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝐾 ∈ Lat)
5 simp2 1138 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑋𝐵)
6 simp3 1139 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑌𝐵)
7 eqid 2738 . . . 4 (meet‘𝐾) = (meet‘𝐾)
81, 3, 7, 4, 5, 6latcl2 18285 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
98simpld 496 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom )
101, 2, 3, 4, 5, 6, 9lejoin1 18233 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑋 (𝑋 𝑌))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088   = wceq 1542  wcel 2107  cop 4591   class class class wbr 5104  dom cdm 5632  cfv 6494  (class class class)co 7352  Basecbs 17043  lecple 17100  joincjn 18160  meetcmee 18161  Latclat 18280
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7665
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-ral 3064  df-rex 3073  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-iun 4955  df-br 5105  df-opab 5167  df-mpt 5188  df-id 5530  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6446  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-riota 7308  df-ov 7355  df-oprab 7356  df-lub 18195  df-join 18197  df-lat 18281
This theorem is referenced by:  latjlej1  18302  latnlej  18305  latnlej2  18308  latjidm  18311  latnle  18322  latabs2  18325  latmlej11  18327  latjass  18332  mod1ile  18342  lubun  18364  oldmm1  37611  olj01  37619  omllaw5N  37641  cvlexchb1  37724  cvlsupr2  37737  cvlsupr7  37742  hlatlej1  37769  hlrelat5N  37796  2atjm  37840  2llnmj  37955  lplnexllnN  37959  2llnjaN  37961  2llnm2N  37963  4atlem3a  37992  2lplnja  38014  2lplnm2N  38016  2lplnmj  38017  dalemply  38049  dalemsly  38050  dalem10  38068  dalem13  38071  dalem21  38089  dalem55  38122  2llnma1b  38181  cdlema1N  38186  elpaddn0  38195  paddasslem12  38226  paddasslem13  38227  pmapjoin  38247  dalawlem2  38267  dalawlem7  38272  dalawlem11  38276  dalawlem12  38277  lhpmcvr3  38420  lhpmcvr5N  38422  lhpmcvr6N  38423  lautj  38488  trljat1  38561  cdlemc1  38586  cdlemc4  38589  cdleme1  38622  cdleme8  38645  cdleme11g  38660  cdleme22e  38739  cdleme22eALTN  38740  cdleme23b  38745  cdleme23c  38746  cdleme27N  38764  cdleme30a  38773  cdleme35fnpq  38844  cdleme35b  38845  cdleme35c  38846  cdleme42h  38877  cdleme42i  38878  cdleme48bw  38897  cdlemg2fv2  38995  cdlemg7fvbwN  39002  cdlemg8b  39023  cdlemg11b  39037  trlcolem  39121  trljco  39135  cdlemi1  39213  cdlemk48  39345  cdlemn2  39590  dihjustlem  39611  dihord1  39613  dihord5apre  39657  dihglbcpreN  39695  dihmeetlem3N  39700  dihmeetlem11N  39712
  Copyright terms: Public domain W3C validator