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

Theorem latlej1 17182
Description: A join's first argument is less than or equal to the join. (chub1 28596 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 1128 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝐾 ∈ Lat)
5 simp2 1129 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑋𝐵)
6 simp3 1130 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑌𝐵)
7 eqid 2724 . . . 4 (meet‘𝐾) = (meet‘𝐾)
81, 3, 7, 4, 5, 6latcl2 17170 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
98simpld 477 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom )
101, 2, 3, 4, 5, 6, 9lejoin1 17134 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑋 (𝑋 𝑌))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072   = wceq 1596  wcel 2103  cop 4291   class class class wbr 4760  dom cdm 5218  cfv 6001  (class class class)co 6765  Basecbs 15980  lecple 16071  joincjn 17066  meetcmee 17067  Latclat 17167
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-ral 3019  df-rex 3020  df-reu 3021  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-id 5128  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-oprab 6769  df-lub 17096  df-join 17098  df-lat 17168
This theorem is referenced by:  latjlej1  17187  latnlej  17190  latnlej2  17193  latjidm  17196  latnle  17207  latabs2  17210  latmlej11  17212  latjass  17217  mod1ile  17227  lubun  17245  oldmm1  34924  olj01  34932  omllaw5N  34954  cvlexchb1  35037  cvlsupr2  35050  cvlsupr7  35055  hlatlej1  35081  hlrelat5N  35107  2atjm  35151  2llnmj  35266  lplnexllnN  35270  2llnjaN  35272  2llnm2N  35274  4atlem3a  35303  2lplnja  35325  2lplnm2N  35327  2lplnmj  35328  dalemply  35360  dalemsly  35361  dalem10  35379  dalem13  35382  dalem21  35400  dalem55  35433  2llnma1b  35492  cdlema1N  35497  elpaddn0  35506  paddasslem12  35537  paddasslem13  35538  pmapjoin  35558  dalawlem2  35578  dalawlem7  35583  dalawlem11  35587  dalawlem12  35588  lhpmcvr3  35731  lhpmcvr5N  35733  lhpmcvr6N  35734  lautj  35799  trljat1  35873  cdlemc1  35898  cdlemc4  35901  cdleme1  35934  cdleme8  35957  cdleme11g  35972  cdleme22e  36051  cdleme22eALTN  36052  cdleme23b  36057  cdleme23c  36058  cdleme27N  36076  cdleme30a  36085  cdleme35fnpq  36156  cdleme35b  36157  cdleme35c  36158  cdleme42h  36189  cdleme42i  36190  cdleme48bw  36209  cdlemg2fv2  36307  cdlemg7fvbwN  36314  cdlemg8b  36335  cdlemg11b  36349  trlcolem  36433  trljco  36447  cdlemi1  36525  cdlemk48  36657  cdlemn2  36903  dihjustlem  36924  dihord1  36926  dihord5apre  36970  dihglbcpreN  37008  dihmeetlem3N  37013  dihmeetlem11N  37025
  Copyright terms: Public domain W3C validator