Theorem hlatlej1 36515

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

Syntax hints:   → wi 4   ∧ w3a 1083   = wceq 1536   ∈ wcel 2113   class class class wbr 5069  ‘cfv 6358  (class class class)co 7159  Basecbs 16486  lecple 16575  joincjn 17557  Latclat 17658  Atomscatm 36403  HLchlt 36490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-reu 3148  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-iun 4924  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-riota 7117  df-ov 7162  df-oprab 7163  df-lub 17587  df-join 17589  df-lat 17659  df-ats 36407  df-atl 36438  df-cvlat 36462  df-hlat 36491

This theorem is referenced by:  hlatlej2  36516  cvratlem  36561  cvrat4  36583  ps-2  36618  lplnllnneN  36696  dalem1  36799  lnatexN  36919  lncmp  36923  2atm2atN  36925  2llnma3r  36928  dalawlem3  37013  dalawlem6  37016  dalawlem7  37017  dalawlem12  37022  trlval4  37328  cdlemc5  37335  cdlemc6  37336  cdlemd3  37340  cdleme0cp  37354  cdleme3h  37375  cdleme5  37380  cdleme9  37393  cdleme11c  37401  cdleme15b  37415  cdleme17b  37427  cdleme19a  37443  cdleme20c  37451  cdleme20j  37458  cdleme21c  37467  cdleme22b  37481  cdleme22d  37483  cdleme22e  37484  cdleme22eALTN  37485  cdleme35e  37593  cdleme35f  37594  cdleme42a  37611  cdleme17d2  37635  cdlemeg46req  37669  cdlemg13a  37791  cdlemg17a  37801  cdlemg18b  37819  cdlemg27a  37832  trlcoabs2N  37862  cdlemg42  37869  cdlemk4  37974  cdlemk1u  37999  cdlemk39  38056  dia2dimlem1  38204  dia2dimlem2  38205  dia2dimlem3  38206  cdlemm10N  38258  cdlemn10  38346  dihjatcclem1  38558