Theorem hlatlej2 38115

Description: A join's second argument is less than or equal to the join. Special case of latlej2 18386 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 38114	. . 3 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → 𝑄 ≤ (𝑄 ∨ 𝑃))
5	4	3com23 1126	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑄 ≤ (𝑄 ∨ 𝑃))
6	2, 3	hlatjcom 38107	. 2 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑃))
7	5, 6	breqtrrd 5170	1 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑄 ≤ (𝑃 ∨ 𝑄))

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   class class class wbr 5142  ‘cfv 6533  (class class class)co 7394  lecple 17188  joincjn 18248  Atomscatm 38002  HLchlt 38089

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 5279  ax-sep 5293  ax-nul 5300  ax-pow 5357  ax-pr 5421  ax-un 7709

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 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5568  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-rn 5681  df-res 5682  df-ima 5683  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7350  df-ov 7397  df-oprab 7398  df-lub 18283  df-join 18285  df-lat 18369  df-ats 38006  df-atl 38037  df-cvlat 38061  df-hlat 38090

This theorem is referenced by:  2llnne2N  38148  cvrat3  38182  cvrat4  38183  hlatexch3N  38220  hlatexch4  38221  dalem3  38404  dalem25  38438  lnatexN  38519  lncmp  38523  2llnma3r  38528  paddasslem5  38564  dalawlem3  38613  dalawlem6  38616  dalawlem7  38617  dalawlem12  38622  lhp2atne  38774  lhp2at0ne  38776  4atexlemunv  38806  cdlemc2  38932  cdlemc5  38935  cdleme3h  38975  cdleme7  38989  cdleme9  38993  cdleme11c  39001  cdleme11dN  39002  cdleme11j  39007  cdleme16b  39019  cdleme17b  39027  cdleme18a  39031  cdleme18b  39032  cdleme18c  39033  cdleme19a  39043  cdleme20d  39052  cdleme20j  39058  cdleme21ct  39069  cdleme22a  39080  cdleme22e  39084  cdleme22eALTN  39085  cdleme35b  39190  cdlemg9a  39372  cdlemg12a  39383  cdlemg13a  39391  cdlemg17a  39401  cdlemg17g  39407  cdlemg18c  39420  cdlemg33b0  39441  cdlemg46  39475  cdlemh1  39555  cdlemh  39557  cdlemk4  39574  cdlemki  39581  cdlemksv2  39587  cdlemk12  39590  cdlemk15  39595  cdlemk12u  39612  cdlemkid1  39662  dia2dimlem1  39804  dia2dimlem3  39806  cdlemn10  39946  dihjatcclem1  40158