Theorem hlatlej1 39809

Description: A join's first argument is less than or equal to the join. Special case of latlej1 18403 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 39797	. 2 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
2		eqid 2735	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
3		hlatlej.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
4	2, 3	atbase 39723	. 2 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
5	2, 3	atbase 39723	. 2 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾))
6		hlatlej.l	. . 3 ⊢ ≤ = (le‘𝐾)
7		hlatlej.j	. . 3 ⊢ ∨ = (join‘𝐾)
8	2, 6, 7	latlej1 18403	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → 𝑃 ≤ (𝑃 ∨ 𝑄))
9	1, 4, 5, 8	syl3an 1161	1 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑃 ≤ (𝑃 ∨ 𝑄))

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   class class class wbr 5074  ‘cfv 6487  (class class class)co 7356  Basecbs 17168  lecple 17216  joincjn 18266  Latclat 18386  Atomscatm 39697  HLchlt 39784

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 2184  ax-ext 2707  ax-rep 5201  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7678

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 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-ral 3050  df-rex 3060  df-rmo 3340  df-reu 3341  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-iun 4925  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-riota 7313  df-ov 7359  df-oprab 7360  df-lub 18299  df-join 18301  df-lat 18387  df-ats 39701  df-atl 39732  df-cvlat 39756  df-hlat 39785

This theorem is referenced by:  hlatlej2  39810  cvratlem  39855  cvrat4  39877  ps-2  39912  lplnllnneN  39990  dalem1  40093  lnatexN  40213  lncmp  40217  2atm2atN  40219  2llnma3r  40222  dalawlem3  40307  dalawlem6  40310  dalawlem7  40311  dalawlem12  40316  trlval4  40622  cdlemc5  40629  cdlemc6  40630  cdlemd3  40634  cdleme0cp  40648  cdleme3h  40669  cdleme5  40674  cdleme9  40687  cdleme11c  40695  cdleme15b  40709  cdleme17b  40721  cdleme19a  40737  cdleme20c  40745  cdleme20j  40752  cdleme21c  40761  cdleme22b  40775  cdleme22d  40777  cdleme22e  40778  cdleme22eALTN  40779  cdleme35e  40887  cdleme35f  40888  cdleme42a  40905  cdleme17d2  40929  cdlemeg46req  40963  cdlemg13a  41085  cdlemg17a  41095  cdlemg18b  41113  cdlemg27a  41126  trlcoabs2N  41156  cdlemg42  41163  cdlemk4  41268  cdlemk1u  41293  cdlemk39  41350  dia2dimlem1  41498  dia2dimlem2  41499  dia2dimlem3  41500  cdlemm10N  41552  cdlemn10  41640  dihjatcclem1  41852