Theorem hlatlej2 39376

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   class class class wbr 5110  ‘cfv 6514  (class class class)co 7390  lecple 17234  joincjn 18279  Atomscatm 39263  HLchlt 39350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-lub 18312  df-join 18314  df-lat 18398  df-ats 39267  df-atl 39298  df-cvlat 39322  df-hlat 39351

This theorem is referenced by:  2llnne2N  39409  cvrat3  39443  cvrat4  39444  hlatexch3N  39481  hlatexch4  39482  dalem3  39665  dalem25  39699  lnatexN  39780  lncmp  39784  2llnma3r  39789  paddasslem5  39825  dalawlem3  39874  dalawlem6  39877  dalawlem7  39878  dalawlem12  39883  lhp2atne  40035  lhp2at0ne  40037  4atexlemunv  40067  cdlemc2  40193  cdlemc5  40196  cdleme3h  40236  cdleme7  40250  cdleme9  40254  cdleme11c  40262  cdleme11dN  40263  cdleme11j  40268  cdleme16b  40280  cdleme17b  40288  cdleme18a  40292  cdleme18b  40293  cdleme18c  40294  cdleme19a  40304  cdleme20d  40313  cdleme20j  40319  cdleme21ct  40330  cdleme22a  40341  cdleme22e  40345  cdleme22eALTN  40346  cdleme35b  40451  cdlemg9a  40633  cdlemg12a  40644  cdlemg13a  40652  cdlemg17a  40662  cdlemg17g  40668  cdlemg18c  40681  cdlemg33b0  40702  cdlemg46  40736  cdlemh1  40816  cdlemh  40818  cdlemk4  40835  cdlemki  40842  cdlemksv2  40848  cdlemk12  40851  cdlemk15  40856  cdlemk12u  40873  cdlemkid1  40923  dia2dimlem1  41065  dia2dimlem3  41067  cdlemn10  41207  dihjatcclem1  41419