Theorem latlej1 18411

Description: A join's first argument is less than or equal to the join. (chub1 31599 analog.) (Contributed by NM, 17-Sep-2011.)

Hypotheses

Ref	Expression
latlej.b	⊢ 𝐵 = (Base‘𝐾)
latlej.l	⊢ ≤ = (le‘𝐾)
latlej.j	⊢ ∨ = (join‘𝐾)

Assertion

Ref	Expression
latlej1	⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ≤ (𝑋 ∨ 𝑌))

Proof of Theorem latlej1

Step	Hyp	Ref	Expression
1		latlej.b	. 2 ⊢ 𝐵 = (Base‘𝐾)
2		latlej.l	. 2 ⊢ ≤ = (le‘𝐾)
3		latlej.j	. 2 ⊢ ∨ = (join‘𝐾)
4		simp1 1137	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat)
5		simp2 1138	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵)
6		simp3 1139	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵)
7		eqid 2737	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
8	1, 3, 7, 4, 5, 6	latcl2 18399	. . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
9	8	simpld 494	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
10	1, 2, 3, 4, 5, 6, 9	lejoin1 18345	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ≤ (𝑋 ∨ 𝑌))

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ⟨cop 4574   class class class wbr 5086  dom cdm 5628  ‘cfv 6496  (class class class)co 7364  Basecbs 17176  lecple 17224  joincjn 18274  meetcmee 18275  Latclat 18394

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 5213  ax-sep 5232  ax-nul 5242  ax-pow 5306  ax-pr 5374  ax-un 7686

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 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5523  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7321  df-ov 7367  df-oprab 7368  df-lub 18307  df-join 18309  df-lat 18395

This theorem is referenced by:  latjlej1  18416  latnlej  18419  latnlej2  18422  latjidm  18425  latnle  18436  latabs2  18439  latmlej11  18441  latjass  18446  mod1ile  18456  lubun  18478  oldmm1  39685  olj01  39693  omllaw5N  39715  cvlexchb1  39798  cvlsupr2  39811  cvlsupr7  39816  hlatlej1  39843  hlrelat5N  39869  2atjm  39913  2llnmj  40028  lplnexllnN  40032  2llnjaN  40034  2llnm2N  40036  4atlem3a  40065  2lplnja  40087  2lplnm2N  40089  2lplnmj  40090  dalemply  40122  dalemsly  40123  dalem10  40141  dalem13  40144  dalem21  40162  dalem55  40195  2llnma1b  40254  cdlema1N  40259  elpaddn0  40268  paddasslem12  40299  paddasslem13  40300  pmapjoin  40320  dalawlem2  40340  dalawlem7  40345  dalawlem11  40349  dalawlem12  40350  lhpmcvr3  40493  lhpmcvr5N  40495  lhpmcvr6N  40496  lautj  40561  trljat1  40634  cdlemc1  40659  cdlemc4  40662  cdleme1  40695  cdleme8  40718  cdleme11g  40733  cdleme22e  40812  cdleme22eALTN  40813  cdleme23b  40818  cdleme23c  40819  cdleme27N  40837  cdleme30a  40846  cdleme35fnpq  40917  cdleme35b  40918  cdleme35c  40919  cdleme42h  40950  cdleme42i  40951  cdleme48bw  40970  cdlemg2fv2  41068  cdlemg7fvbwN  41075  cdlemg8b  41096  cdlemg11b  41110  trlcolem  41194  trljco  41208  cdlemi1  41286  cdlemk48  41418  cdlemn2  41663  dihjustlem  41684  dihord1  41686  dihord5apre  41730  dihglbcpreN  41768  dihmeetlem3N  41773  dihmeetlem11N  41785