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

Theorem latlej1 15546
Description: A join's first argument is less than or equal to the join. (chub1 26117 analog.) (Contributed by NM, 17-Sep-2011.)
Hypotheses
Ref Expression
latlej.b  |-  B  =  ( Base `  K
)
latlej.l  |-  .<_  =  ( le `  K )
latlej.j  |-  .\/  =  ( join `  K )
Assertion
Ref Expression
latlej1  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  X  .<_  ( X  .\/  Y ) )

Proof of Theorem latlej1
StepHypRef Expression
1 latlej.b . 2  |-  B  =  ( Base `  K
)
2 latlej.l . 2  |-  .<_  =  ( le `  K )
3 latlej.j . 2  |-  .\/  =  ( join `  K )
4 simp1 996 . 2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  K  e.  Lat )
5 simp2 997 . 2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  X  e.  B )
6 simp3 998 . 2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  Y  e.  B )
7 eqid 2467 . . . 4  |-  ( meet `  K )  =  (
meet `  K )
81, 3, 7, 4, 5, 6latcl2 15534 . . 3  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  ( <. X ,  Y >.  e.  dom  .\/  /\  <. X ,  Y >.  e. 
dom  ( meet `  K
) ) )
98simpld 459 . 2  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  -> 
<. X ,  Y >.  e. 
dom  .\/  )
101, 2, 3, 4, 5, 6, 9lejoin1 15498 1  |-  ( ( K  e.  Lat  /\  X  e.  B  /\  Y  e.  B )  ->  X  .<_  ( X  .\/  Y ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973    = wceq 1379    e. wcel 1767   <.cop 4033   class class class wbr 4447   dom cdm 4999   ` cfv 5587  (class class class)co 6283   Basecbs 14489   lecple 14561   joincjn 15430   meetcmee 15431   Latclat 15531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6575
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5550  df-fun 5589  df-fn 5590  df-f 5591  df-f1 5592  df-fo 5593  df-f1o 5594  df-fv 5595  df-riota 6244  df-ov 6286  df-oprab 6287  df-lub 15460  df-join 15462  df-lat 15532
This theorem is referenced by:  latjlej1  15551  latnlej  15554  latnlej2  15557  latjidm  15560  latnle  15571  latabs2  15574  latmlej11  15576  latjass  15581  mod1ile  15591  lubun  15609  oldmm1  34023  olj01  34031  omllaw5N  34053  cvlexchb1  34136  cvlsupr2  34149  cvlsupr7  34154  hlatlej1  34180  hlrelat5N  34206  2atjm  34250  2llnmj  34365  lplnexllnN  34369  2llnjaN  34371  2llnm2N  34373  4atlem3a  34402  2lplnja  34424  2lplnm2N  34426  2lplnmj  34427  dalemply  34459  dalemsly  34460  dalem10  34478  dalem13  34481  dalem21  34499  dalem55  34532  2llnma1b  34591  cdlema1N  34596  elpaddn0  34605  paddasslem12  34636  paddasslem13  34637  pmapjoin  34657  dalawlem2  34677  dalawlem7  34682  dalawlem11  34686  dalawlem12  34687  lhpmcvr3  34830  lhpmcvr5N  34832  lhpmcvr6N  34833  lautj  34898  trljat1  34971  cdlemc1  34996  cdlemc4  34999  cdleme1  35032  cdleme8  35055  cdleme11g  35070  cdleme22e  35149  cdleme22eALTN  35150  cdleme23b  35155  cdleme23c  35156  cdleme27N  35174  cdleme30a  35183  cdleme35fnpq  35254  cdleme35b  35255  cdleme35c  35256  cdleme42h  35287  cdleme42i  35288  cdleme48bw  35307  cdlemg2fv2  35405  cdlemg7fvbwN  35412  cdlemg8b  35433  cdlemg11b  35447  trlcolem  35531  trljco  35545  cdlemi1  35623  cdlemk48  35755  cdlemn2  36001  dihjustlem  36022  dihord1  36024  dihord5apre  36068  dihglbcpreN  36106  dihmeetlem3N  36111  dihmeetlem11N  36123
  Copyright terms: Public domain W3C validator