Theorem hlatlej2 40001

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

Syntax hints:   → wi 4   ∧ w3a 1099   = wceq 1561   ∈ wcel 2143   class class class wbr 5101  ‘cfv 6522  (class class class)co 7397  lecple 17294  joincjn 18344  Atomscatm 39888  HLchlt 39975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5228  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7719

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6478  df-fun 6524  df-fn 6525  df-f 6526  df-f1 6527  df-fo 6528  df-f1o 6529  df-fv 6530  df-riota 7354  df-ov 7400  df-oprab 7401  df-lub 18377  df-join 18379  df-lat 18465  df-ats 39892  df-atl 39923  df-cvlat 39947  df-hlat 39976

This theorem is referenced by:  2llnne2N  40033  cvrat3  40067  cvrat4  40068  hlatexch3N  40105  hlatexch4  40106  dalem3  40289  dalem25  40323  lnatexN  40404  lncmp  40408  2llnma3r  40413  paddasslem5  40449  dalawlem3  40498  dalawlem6  40501  dalawlem7  40502  dalawlem12  40507  lhp2atne  40659  lhp2at0ne  40661  4atexlemunv  40691  cdlemc2  40817  cdlemc5  40820  cdleme3h  40860  cdleme7  40874  cdleme9  40878  cdleme11c  40886  cdleme11dN  40887  cdleme11j  40892  cdleme16b  40904  cdleme17b  40912  cdleme18a  40916  cdleme18b  40917  cdleme18c  40918  cdleme19a  40928  cdleme20d  40937  cdleme20j  40943  cdleme21ct  40954  cdleme22a  40965  cdleme22e  40969  cdleme22eALTN  40970  cdleme35b  41075  cdlemg9a  41257  cdlemg12a  41268  cdlemg13a  41276  cdlemg17a  41286  cdlemg17g  41292  cdlemg18c  41305  cdlemg33b0  41326  cdlemg46  41360  cdlemh1  41440  cdlemh  41442  cdlemk4  41459  cdlemki  41466  cdlemksv2  41472  cdlemk12  41475  cdlemk15  41480  cdlemk12u  41497  cdlemkid1  41547  dia2dimlem1  41689  dia2dimlem3  41691  cdlemn10  41831  dihjatcclem1  42043