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

Theorem hlatlej1 33042
Description: A join's first argument is less than or equal to the join. Special case of latlej1 15249 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
hlatlej1  |-  ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  ->  P  .<_  ( P  .\/  Q ) )

Proof of Theorem hlatlej1
StepHypRef Expression
1 hllat 33031 . 2  |-  ( K  e.  HL  ->  K  e.  Lat )
2 eqid 2443 . . 3  |-  ( Base `  K )  =  (
Base `  K )
3 hlatlej.a . . 3  |-  A  =  ( Atoms `  K )
42, 3atbase 32957 . 2  |-  ( P  e.  A  ->  P  e.  ( Base `  K
) )
52, 3atbase 32957 . 2  |-  ( Q  e.  A  ->  Q  e.  ( Base `  K
) )
6 hlatlej.l . . 3  |-  .<_  =  ( le `  K )
7 hlatlej.j . . 3  |-  .\/  =  ( join `  K )
82, 6, 7latlej1 15249 . 2  |-  ( ( K  e.  Lat  /\  P  e.  ( Base `  K )  /\  Q  e.  ( Base `  K
) )  ->  P  .<_  ( P  .\/  Q
) )
91, 4, 5, 8syl3an 1260 1  |-  ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  ->  P  .<_  ( P  .\/  Q ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965    = wceq 1369    e. wcel 1756   class class class wbr 4311   ` cfv 5437  (class class class)co 6110   Basecbs 14193   lecple 14264   joincjn 15133   Latclat 15234   Atomscatm 32931   HLchlt 33018
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 4422  ax-sep 4432  ax-nul 4440  ax-pow 4489  ax-pr 4550  ax-un 6391
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 2577  df-ne 2622  df-ral 2739  df-rex 2740  df-reu 2741  df-rab 2743  df-v 2993  df-sbc 3206  df-csb 3308  df-dif 3350  df-un 3352  df-in 3354  df-ss 3361  df-nul 3657  df-if 3811  df-pw 3881  df-sn 3897  df-pr 3899  df-op 3903  df-uni 4111  df-iun 4192  df-br 4312  df-opab 4370  df-mpt 4371  df-id 4655  df-xp 4865  df-rel 4866  df-cnv 4867  df-co 4868  df-dm 4869  df-rn 4870  df-res 4871  df-ima 4872  df-iota 5400  df-fun 5439  df-fn 5440  df-f 5441  df-f1 5442  df-fo 5443  df-f1o 5444  df-fv 5445  df-riota 6071  df-ov 6113  df-oprab 6114  df-lub 15163  df-join 15165  df-lat 15235  df-ats 32935  df-atl 32966  df-cvlat 32990  df-hlat 33019
This theorem is referenced by:  hlatlej2  33043  cvratlem  33088  cvrat4  33110  ps-2  33145  lplnllnneN  33223  dalem1  33326  lnatexN  33446  lncmp  33450  2atm2atN  33452  2llnma3r  33455  dalawlem3  33540  dalawlem6  33543  dalawlem7  33544  dalawlem12  33549  trlval4  33855  cdlemc5  33862  cdlemc6  33863  cdlemd3  33867  cdleme0cp  33881  cdleme3h  33902  cdleme5  33907  cdleme9  33920  cdleme11c  33928  cdleme15b  33942  cdleme17b  33954  cdleme19a  33970  cdleme20c  33978  cdleme20j  33985  cdleme21c  33994  cdleme22b  34008  cdleme22d  34010  cdleme22e  34011  cdleme22eALTN  34012  cdleme35e  34120  cdleme35f  34121  cdleme42a  34138  cdleme17d2  34162  cdlemeg46req  34196  cdlemg13a  34318  cdlemg17a  34328  cdlemg18b  34346  cdlemg27a  34359  trlcoabs2N  34389  cdlemg42  34396  cdlemk4  34501  cdlemk1u  34526  cdlemk39  34583  dia2dimlem1  34732  dia2dimlem2  34733  dia2dimlem3  34734  cdlemm10N  34786  cdlemn10  34874  dihjatcclem1  35086
  Copyright terms: Public domain W3C validator