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

Theorem hlatlej1 36380
Description: A join's first argument is less than or equal to the join. Special case of latlej1 17662 to show an atom is on a line. (Contributed by NM, 15-May-2013.)
Hypotheses
Ref Expression
hlatlej.l = (le‘𝐾)
hlatlej.j = (join‘𝐾)
hlatlej.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
hlatlej1 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → 𝑃 (𝑃 𝑄))

Proof of Theorem hlatlej1
StepHypRef Expression
1 hllat 36368 . 2 (𝐾 ∈ HL → 𝐾 ∈ Lat)
2 eqid 2825 . . 3 (Base‘𝐾) = (Base‘𝐾)
3 hlatlej.a . . 3 𝐴 = (Atoms‘𝐾)
42, 3atbase 36294 . 2 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
52, 3atbase 36294 . 2 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
6 hlatlej.l . . 3 = (le‘𝐾)
7 hlatlej.j . . 3 = (join‘𝐾)
82, 6, 7latlej1 17662 . 2 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → 𝑃 (𝑃 𝑄))
91, 4, 5, 8syl3an 1154 1 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → 𝑃 (𝑃 𝑄))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1081   = wceq 1530  wcel 2107   class class class wbr 5062  cfv 6351  (class class class)co 7151  Basecbs 16475  lecple 16564  joincjn 17546  Latclat 17647  Atomscatm 36268  HLchlt 36355
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-reu 3149  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4837  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-id 5458  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-riota 7109  df-ov 7154  df-oprab 7155  df-lub 17576  df-join 17578  df-lat 17648  df-ats 36272  df-atl 36303  df-cvlat 36327  df-hlat 36356
This theorem is referenced by:  hlatlej2  36381  cvratlem  36426  cvrat4  36448  ps-2  36483  lplnllnneN  36561  dalem1  36664  lnatexN  36784  lncmp  36788  2atm2atN  36790  2llnma3r  36793  dalawlem3  36878  dalawlem6  36881  dalawlem7  36882  dalawlem12  36887  trlval4  37193  cdlemc5  37200  cdlemc6  37201  cdlemd3  37205  cdleme0cp  37219  cdleme3h  37240  cdleme5  37245  cdleme9  37258  cdleme11c  37266  cdleme15b  37280  cdleme17b  37292  cdleme19a  37308  cdleme20c  37316  cdleme20j  37323  cdleme21c  37332  cdleme22b  37346  cdleme22d  37348  cdleme22e  37349  cdleme22eALTN  37350  cdleme35e  37458  cdleme35f  37459  cdleme42a  37476  cdleme17d2  37500  cdlemeg46req  37534  cdlemg13a  37656  cdlemg17a  37666  cdlemg18b  37684  cdlemg27a  37697  trlcoabs2N  37727  cdlemg42  37734  cdlemk4  37839  cdlemk1u  37864  cdlemk39  37921  dia2dimlem1  38069  dia2dimlem2  38070  dia2dimlem3  38071  cdlemm10N  38123  cdlemn10  38211  dihjatcclem1  38423
  Copyright terms: Public domain W3C validator