Theorem hlatlej2 40170

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

Syntax hints:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143   class class class wbr 5109  ‘cfv 6536  (class class class)co 7410  lecple 17312  joincjn 18362  Atomscatm 40057  HLchlt 40144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-lub 18395  df-join 18397  df-lat 18483  df-ats 40061  df-atl 40092  df-cvlat 40116  df-hlat 40145

This theorem is referenced by:  2llnne2N  40202  cvrat3  40236  cvrat4  40237  hlatexch3N  40274  hlatexch4  40275  dalem3  40458  dalem25  40492  lnatexN  40573  lncmp  40577  2llnma3r  40582  paddasslem5  40618  dalawlem3  40667  dalawlem6  40670  dalawlem7  40671  dalawlem12  40676  lhp2atne  40828  lhp2at0ne  40830  4atexlemunv  40860  cdlemc2  40986  cdlemc5  40989  cdleme3h  41029  cdleme7  41043  cdleme9  41047  cdleme11c  41055  cdleme11dN  41056  cdleme11j  41061  cdleme16b  41073  cdleme17b  41081  cdleme18a  41085  cdleme18b  41086  cdleme18c  41087  cdleme19a  41097  cdleme20d  41106  cdleme20j  41112  cdleme21ct  41123  cdleme22a  41134  cdleme22e  41138  cdleme22eALTN  41139  cdleme35b  41244  cdlemg9a  41426  cdlemg12a  41437  cdlemg13a  41445  cdlemg17a  41455  cdlemg17g  41461  cdlemg18c  41474  cdlemg33b0  41495  cdlemg46  41529  cdlemh1  41609  cdlemh  41611  cdlemk4  41628  cdlemki  41635  cdlemksv2  41641  cdlemk12  41644  cdlemk15  41649  cdlemk12u  41666  cdlemkid1  41716  dia2dimlem1  41858  dia2dimlem3  41860  cdlemn10  42000  dihjatcclem1  42212