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

Theorem hlatlej2 36382
Description: A join's second argument is less than or equal to the join. Special case of latlej2 17664 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
hlatlej2 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → 𝑄 (𝑃 𝑄))

Proof of Theorem hlatlej2
StepHypRef Expression
1 hlatlej.l . . . 4 = (le‘𝐾)
2 hlatlej.j . . . 4 = (join‘𝐾)
3 hlatlej.a . . . 4 𝐴 = (Atoms‘𝐾)
41, 2, 3hlatlej1 36381 . . 3 ((𝐾 ∈ HL ∧ 𝑄𝐴𝑃𝐴) → 𝑄 (𝑄 𝑃))
543com23 1120 . 2 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → 𝑄 (𝑄 𝑃))
62, 3hlatjcom 36374 . 2 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) = (𝑄 𝑃))
75, 6breqtrrd 5090 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  lecple 16565  joincjn 17547  Atomscatm 36269  HLchlt 36356
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 17577  df-join 17579  df-lat 17649  df-ats 36273  df-atl 36304  df-cvlat 36328  df-hlat 36357
This theorem is referenced by:  2llnne2N  36414  cvrat3  36448  cvrat4  36449  hlatexch3N  36486  hlatexch4  36487  dalem3  36670  dalem25  36704  lnatexN  36785  lncmp  36789  2llnma3r  36794  paddasslem5  36830  dalawlem3  36879  dalawlem6  36882  dalawlem7  36883  dalawlem12  36888  lhp2atne  37040  lhp2at0ne  37042  4atexlemunv  37072  cdlemc2  37198  cdlemc5  37201  cdleme3h  37241  cdleme7  37255  cdleme9  37259  cdleme11c  37267  cdleme11dN  37268  cdleme11j  37273  cdleme16b  37285  cdleme17b  37293  cdleme18a  37297  cdleme18b  37298  cdleme18c  37299  cdleme19a  37309  cdleme20d  37318  cdleme20j  37324  cdleme21ct  37335  cdleme22a  37346  cdleme22e  37350  cdleme22eALTN  37351  cdleme35b  37456  cdlemg9a  37638  cdlemg12a  37649  cdlemg13a  37657  cdlemg17a  37667  cdlemg17g  37673  cdlemg18c  37686  cdlemg33b0  37707  cdlemg46  37741  cdlemh1  37821  cdlemh  37823  cdlemk4  37840  cdlemki  37847  cdlemksv2  37853  cdlemk12  37856  cdlemk15  37861  cdlemk12u  37878  cdlemkid1  37928  dia2dimlem1  38070  dia2dimlem3  38072  cdlemn10  38212  dihjatcclem1  38424
  Copyright terms: Public domain W3C validator