Theorem hlatlej2 39756

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   class class class wbr 5100  ‘cfv 6500  (class class class)co 7368  lecple 17196  joincjn 18246  Atomscatm 39643  HLchlt 39730

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-lub 18279  df-join 18281  df-lat 18367  df-ats 39647  df-atl 39678  df-cvlat 39702  df-hlat 39731

This theorem is referenced by:  2llnne2N  39788  cvrat3  39822  cvrat4  39823  hlatexch3N  39860  hlatexch4  39861  dalem3  40044  dalem25  40078  lnatexN  40159  lncmp  40163  2llnma3r  40168  paddasslem5  40204  dalawlem3  40253  dalawlem6  40256  dalawlem7  40257  dalawlem12  40262  lhp2atne  40414  lhp2at0ne  40416  4atexlemunv  40446  cdlemc2  40572  cdlemc5  40575  cdleme3h  40615  cdleme7  40629  cdleme9  40633  cdleme11c  40641  cdleme11dN  40642  cdleme11j  40647  cdleme16b  40659  cdleme17b  40667  cdleme18a  40671  cdleme18b  40672  cdleme18c  40673  cdleme19a  40683  cdleme20d  40692  cdleme20j  40698  cdleme21ct  40709  cdleme22a  40720  cdleme22e  40724  cdleme22eALTN  40725  cdleme35b  40830  cdlemg9a  41012  cdlemg12a  41023  cdlemg13a  41031  cdlemg17a  41041  cdlemg17g  41047  cdlemg18c  41060  cdlemg33b0  41081  cdlemg46  41115  cdlemh1  41195  cdlemh  41197  cdlemk4  41214  cdlemki  41221  cdlemksv2  41227  cdlemk12  41230  cdlemk15  41235  cdlemk12u  41252  cdlemkid1  41302  dia2dimlem1  41444  dia2dimlem3  41446  cdlemn10  41586  dihjatcclem1  41798