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

Theorem latlej1 17661
Description: A join's first argument is less than or equal to the join. (chub1 29288 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 1133 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝐾 ∈ Lat)
5 simp2 1134 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑋𝐵)
6 simp3 1135 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑌𝐵)
7 eqid 2822 . . . 4 (meet‘𝐾) = (meet‘𝐾)
81, 3, 7, 4, 5, 6latcl2 17649 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
98simpld 498 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom )
101, 2, 3, 4, 5, 6, 9lejoin1 17613 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑋 (𝑋 𝑌))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084   = wceq 1538  wcel 2114  cop 4545   class class class wbr 5042  dom cdm 5532  cfv 6334  (class class class)co 7140  Basecbs 16474  lecple 16563  joincjn 17545  meetcmee 17546  Latclat 17646
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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-ral 3135  df-rex 3136  df-reu 3137  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5437  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-riota 7098  df-ov 7143  df-oprab 7144  df-lub 17575  df-join 17577  df-lat 17647
This theorem is referenced by:  latjlej1  17666  latnlej  17669  latnlej2  17672  latjidm  17675  latnle  17686  latabs2  17689  latmlej11  17691  latjass  17696  mod1ile  17706  lubun  17724  oldmm1  36472  olj01  36480  omllaw5N  36502  cvlexchb1  36585  cvlsupr2  36598  cvlsupr7  36603  hlatlej1  36630  hlrelat5N  36656  2atjm  36700  2llnmj  36815  lplnexllnN  36819  2llnjaN  36821  2llnm2N  36823  4atlem3a  36852  2lplnja  36874  2lplnm2N  36876  2lplnmj  36877  dalemply  36909  dalemsly  36910  dalem10  36928  dalem13  36931  dalem21  36949  dalem55  36982  2llnma1b  37041  cdlema1N  37046  elpaddn0  37055  paddasslem12  37086  paddasslem13  37087  pmapjoin  37107  dalawlem2  37127  dalawlem7  37132  dalawlem11  37136  dalawlem12  37137  lhpmcvr3  37280  lhpmcvr5N  37282  lhpmcvr6N  37283  lautj  37348  trljat1  37421  cdlemc1  37446  cdlemc4  37449  cdleme1  37482  cdleme8  37505  cdleme11g  37520  cdleme22e  37599  cdleme22eALTN  37600  cdleme23b  37605  cdleme23c  37606  cdleme27N  37624  cdleme30a  37633  cdleme35fnpq  37704  cdleme35b  37705  cdleme35c  37706  cdleme42h  37737  cdleme42i  37738  cdleme48bw  37757  cdlemg2fv2  37855  cdlemg7fvbwN  37862  cdlemg8b  37883  cdlemg11b  37897  trlcolem  37981  trljco  37995  cdlemi1  38073  cdlemk48  38205  cdlemn2  38450  dihjustlem  38471  dihord1  38473  dihord5apre  38517  dihglbcpreN  38555  dihmeetlem3N  38560  dihmeetlem11N  38572
  Copyright terms: Public domain W3C validator