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

Theorem hlatlej2 33020
Description: A join's second argument is less than or equal to the join. Special case of latlej2 15231 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 33019 . . 3  |-  ( ( K  e.  HL  /\  Q  e.  A  /\  P  e.  A )  ->  Q  .<_  ( Q  .\/  P ) )
543com23 1193 . 2  |-  ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  ->  Q  .<_  ( Q  .\/  P ) )
62, 3hlatjcom 33012 . 2  |-  ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  ->  ( P  .\/  Q
)  =  ( Q 
.\/  P ) )
75, 6breqtrrd 4318 1  |-  ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  ->  Q  .<_  ( P  .\/  Q ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965    = wceq 1369    e. wcel 1756   class class class wbr 4292   ` cfv 5418  (class class class)co 6091   lecple 14245   joincjn 15114   Atomscatm 32908   HLchlt 32995
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4403  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-reu 2722  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-iun 4173  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-riota 6052  df-ov 6094  df-oprab 6095  df-lub 15144  df-join 15146  df-lat 15216  df-ats 32912  df-atl 32943  df-cvlat 32967  df-hlat 32996
This theorem is referenced by:  2llnne2N  33052  cvrat3  33086  cvrat4  33087  hlatexch3N  33124  hlatexch4  33125  dalem3  33308  dalem25  33342  lnatexN  33423  lncmp  33427  2llnma3r  33432  paddasslem5  33468  dalawlem3  33517  dalawlem6  33520  dalawlem7  33521  dalawlem12  33526  lhp2atne  33678  lhp2at0ne  33680  4atexlemunv  33710  cdlemc2  33836  cdlemc5  33839  cdleme3h  33879  cdleme7  33893  cdleme9  33897  cdleme11c  33905  cdleme11dN  33906  cdleme11j  33911  cdleme16b  33923  cdleme17b  33931  cdleme18a  33935  cdleme18b  33936  cdleme18c  33937  cdleme20y  33946  cdleme19a  33947  cdleme20d  33956  cdleme20j  33962  cdleme21ct  33973  cdleme22a  33984  cdleme22e  33988  cdleme22eALTN  33989  cdleme35b  34094  cdlemg9a  34276  cdlemg12a  34287  cdlemg13a  34295  cdlemg17a  34305  cdlemg17g  34311  cdlemg18c  34324  cdlemg33b0  34345  cdlemg46  34379  cdlemh1  34459  cdlemh  34461  cdlemk4  34478  cdlemki  34485  cdlemksv2  34491  cdlemk12  34494  cdlemk15  34499  cdlemk12u  34516  cdlemkid1  34566  dia2dimlem1  34709  dia2dimlem3  34711  cdlemn10  34851  dihjatcclem1  35063
  Copyright terms: Public domain W3C validator