Theorem hlatlej2 38234

Description: A join's second argument is less than or equal to the join. Special case of latlej2 18398 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

Step	Hyp	Ref	Expression
1		hlatlej.l	. . . 4 ⊢ ≤ = (le‘𝐾)
2		hlatlej.j	. . . 4 ⊢ ∨ = (join‘𝐾)
3		hlatlej.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
4	1, 2, 3	hlatlej1 38233	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → 𝑄 ≤ (𝑄 ∨ 𝑃))
5	4	3com23 1126	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑄 ≤ (𝑄 ∨ 𝑃))
6	2, 3	hlatjcom 38226	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑃))
7	5, 6	breqtrrd 5175	1 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑄 ≤ (𝑃 ∨ 𝑄))

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   class class class wbr 5147  ‘cfv 6540  (class class class)co 7405  lecple 17200  joincjn 18260  Atomscatm 38121  HLchlt 38208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-lub 18295  df-join 18297  df-lat 18381  df-ats 38125  df-atl 38156  df-cvlat 38180  df-hlat 38209

This theorem is referenced by:  2llnne2N  38267  cvrat3  38301  cvrat4  38302  hlatexch3N  38339  hlatexch4  38340  dalem3  38523  dalem25  38557  lnatexN  38638  lncmp  38642  2llnma3r  38647  paddasslem5  38683  dalawlem3  38732  dalawlem6  38735  dalawlem7  38736  dalawlem12  38741  lhp2atne  38893  lhp2at0ne  38895  4atexlemunv  38925  cdlemc2  39051  cdlemc5  39054  cdleme3h  39094  cdleme7  39108  cdleme9  39112  cdleme11c  39120  cdleme11dN  39121  cdleme11j  39126  cdleme16b  39138  cdleme17b  39146  cdleme18a  39150  cdleme18b  39151  cdleme18c  39152  cdleme19a  39162  cdleme20d  39171  cdleme20j  39177  cdleme21ct  39188  cdleme22a  39199  cdleme22e  39203  cdleme22eALTN  39204  cdleme35b  39309  cdlemg9a  39491  cdlemg12a  39502  cdlemg13a  39510  cdlemg17a  39520  cdlemg17g  39526  cdlemg18c  39539  cdlemg33b0  39560  cdlemg46  39594  cdlemh1  39674  cdlemh  39676  cdlemk4  39693  cdlemki  39700  cdlemksv2  39706  cdlemk12  39709  cdlemk15  39714  cdlemk12u  39731  cdlemkid1  39781  dia2dimlem1  39923  dia2dimlem3  39925  cdlemn10  40065  dihjatcclem1  40277