Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hlatlej2 Unicode version

Theorem hlatlej2 29491
Description: A join's second argument is less than or equal to the join. Special case of latlej2 14418 to show an atom is on a line. (Contributed by NM, 15-May-2013.)
Hypotheses
Ref Expression
hlatlej.l  |-  .<_  =  ( le `  K )
hlatlej.j  |-  .\/  =  ( join `  K )
hlatlej.a  |-  A  =  ( Atoms `  K )
Assertion
Ref Expression
hlatlej2  |-  ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  ->  Q  .<_  ( P  .\/  Q ) )

Proof of Theorem hlatlej2
StepHypRef Expression
1 hlatlej.l . . . 4  |-  .<_  =  ( le `  K )
2 hlatlej.j . . . 4  |-  .\/  =  ( join `  K )
3 hlatlej.a . . . 4  |-  A  =  ( Atoms `  K )
41, 2, 3hlatlej1 29490 . . 3  |-  ( ( K  e.  HL  /\  Q  e.  A  /\  P  e.  A )  ->  Q  .<_  ( Q  .\/  P ) )
543com23 1159 . 2  |-  ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  ->  Q  .<_  ( Q  .\/  P ) )
62, 3hlatjcom 29483 . 2  |-  ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  ->  ( P  .\/  Q
)  =  ( Q 
.\/  P ) )
75, 6breqtrrd 4180 1  |-  ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  ->  Q  .<_  ( P  .\/  Q ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936    = wceq 1649    e. wcel 1717   class class class wbr 4154   ` cfv 5395  (class class class)co 6021   lecple 13464   joincjn 14329   Atomscatm 29379   HLchlt 29466
This theorem is referenced by:  2llnne2N  29523  cvrat3  29557  cvrat4  29558  hlatexch3N  29595  hlatexch4  29596  dalem3  29779  dalem25  29813  lnatexN  29894  lncmp  29898  2llnma3r  29903  paddasslem5  29939  dalawlem3  29988  dalawlem6  29991  dalawlem7  29992  dalawlem12  29997  lhp2atne  30149  lhp2at0ne  30151  4atexlemunv  30181  cdlemc2  30307  cdlemc5  30310  cdleme3h  30350  cdleme7  30364  cdleme9  30368  cdleme11c  30376  cdleme11dN  30377  cdleme11j  30382  cdleme16b  30394  cdleme17b  30402  cdleme18a  30406  cdleme18b  30407  cdleme18c  30408  cdleme20y  30417  cdleme19a  30418  cdleme20d  30427  cdleme20j  30433  cdleme21ct  30444  cdleme22a  30455  cdleme22e  30459  cdleme22eALTN  30460  cdleme35b  30565  cdlemg9a  30747  cdlemg12a  30758  cdlemg13a  30766  cdlemg17a  30776  cdlemg17g  30782  cdlemg18c  30795  cdlemg33b0  30816  cdlemg46  30850  cdlemh1  30930  cdlemh  30932  cdlemk4  30949  cdlemki  30956  cdlemksv2  30962  cdlemk12  30965  cdlemk15  30970  cdlemk12u  30987  cdlemkid1  31037  dia2dimlem1  31180  dia2dimlem3  31182  cdlemn10  31322  dihjatcclem1  31534
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-rep 4262  ax-sep 4272  ax-nul 4280  ax-pow 4319  ax-pr 4345  ax-un 4642
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2243  df-mo 2244  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-nel 2554  df-ral 2655  df-rex 2656  df-reu 2657  df-rab 2659  df-v 2902  df-sbc 3106  df-csb 3196  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-pw 3745  df-sn 3764  df-pr 3765  df-op 3767  df-uni 3959  df-iun 4038  df-br 4155  df-opab 4209  df-mpt 4210  df-id 4440  df-xp 4825  df-rel 4826  df-cnv 4827  df-co 4828  df-dm 4829  df-rn 4830  df-res 4831  df-ima 4832  df-iota 5359  df-fun 5397  df-fn 5398  df-f 5399  df-f1 5400  df-fo 5401  df-f1o 5402  df-fv 5403  df-ov 6024  df-oprab 6025  df-mpt2 6026  df-1st 6289  df-2nd 6290  df-undef 6480  df-riota 6486  df-lub 14359  df-join 14361  df-lat 14403  df-ats 29383  df-atl 29414  df-cvlat 29438  df-hlat 29467
  Copyright terms: Public domain W3C validator