Theorem hlatlej1 37396

Description: A join's first argument is less than or equal to the join. Special case of latlej1 18175 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
hlatlej1	⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑃 ≤ (𝑃 ∨ 𝑄))

Proof of Theorem hlatlej1

Step	Hyp	Ref	Expression
1		hllat 37384	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2		eqid 2739	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		hlatlej.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
4	2, 3	atbase 37310	. 2 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
5	2, 3	atbase 37310	. 2 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾))
6		hlatlej.l	. . 3 ⊢ ≤ = (le‘𝐾)
7		hlatlej.j	. . 3 ⊢ ∨ = (join‘𝐾)
8	2, 6, 7	latlej1 18175	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → 𝑃 ≤ (𝑃 ∨ 𝑄))
9	1, 4, 5, 8	syl3an 1159	1 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑃 ≤ (𝑃 ∨ 𝑄))

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107   class class class wbr 5075  ‘cfv 6437  (class class class)co 7284  Basecbs 16921  lecple 16978  joincjn 18038  Latclat 18158  Atomscatm 37284  HLchlt 37371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-lub 18073  df-join 18075  df-lat 18159  df-ats 37288  df-atl 37319  df-cvlat 37343  df-hlat 37372

This theorem is referenced by:  hlatlej2  37397  cvratlem  37442  cvrat4  37464  ps-2  37499  lplnllnneN  37577  dalem1  37680  lnatexN  37800  lncmp  37804  2atm2atN  37806  2llnma3r  37809  dalawlem3  37894  dalawlem6  37897  dalawlem7  37898  dalawlem12  37903  trlval4  38209  cdlemc5  38216  cdlemc6  38217  cdlemd3  38221  cdleme0cp  38235  cdleme3h  38256  cdleme5  38261  cdleme9  38274  cdleme11c  38282  cdleme15b  38296  cdleme17b  38308  cdleme19a  38324  cdleme20c  38332  cdleme20j  38339  cdleme21c  38348  cdleme22b  38362  cdleme22d  38364  cdleme22e  38365  cdleme22eALTN  38366  cdleme35e  38474  cdleme35f  38475  cdleme42a  38492  cdleme17d2  38516  cdlemeg46req  38550  cdlemg13a  38672  cdlemg17a  38682  cdlemg18b  38700  cdlemg27a  38713  trlcoabs2N  38743  cdlemg42  38750  cdlemk4  38855  cdlemk1u  38880  cdlemk39  38937  dia2dimlem1  39085  dia2dimlem2  39086  dia2dimlem3  39087  cdlemm10N  39139  cdlemn10  39227  dihjatcclem1  39439