Theorem latlej1 18414

Description: A join's first argument is less than or equal to the join. (chub1 31443 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 1136	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat)
5		simp2 1137	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵)
6		simp3 1138	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵)
7		eqid 2730	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
8	1, 3, 7, 4, 5, 6	latcl2 18402	. . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
9	8	simpld 494	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
10	1, 2, 3, 4, 5, 6, 9	lejoin1 18350	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ≤ (𝑋 ∨ 𝑌))

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ⟨cop 4598   class class class wbr 5110  dom cdm 5641  ‘cfv 6514  (class class class)co 7390  Basecbs 17186  lecple 17234  joincjn 18279  meetcmee 18280  Latclat 18397

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-lub 18312  df-join 18314  df-lat 18398

This theorem is referenced by:  latjlej1  18419  latnlej  18422  latnlej2  18425  latjidm  18428  latnle  18439  latabs2  18442  latmlej11  18444  latjass  18449  mod1ile  18459  lubun  18481  oldmm1  39217  olj01  39225  omllaw5N  39247  cvlexchb1  39330  cvlsupr2  39343  cvlsupr7  39348  hlatlej1  39375  hlrelat5N  39402  2atjm  39446  2llnmj  39561  lplnexllnN  39565  2llnjaN  39567  2llnm2N  39569  4atlem3a  39598  2lplnja  39620  2lplnm2N  39622  2lplnmj  39623  dalemply  39655  dalemsly  39656  dalem10  39674  dalem13  39677  dalem21  39695  dalem55  39728  2llnma1b  39787  cdlema1N  39792  elpaddn0  39801  paddasslem12  39832  paddasslem13  39833  pmapjoin  39853  dalawlem2  39873  dalawlem7  39878  dalawlem11  39882  dalawlem12  39883  lhpmcvr3  40026  lhpmcvr5N  40028  lhpmcvr6N  40029  lautj  40094  trljat1  40167  cdlemc1  40192  cdlemc4  40195  cdleme1  40228  cdleme8  40251  cdleme11g  40266  cdleme22e  40345  cdleme22eALTN  40346  cdleme23b  40351  cdleme23c  40352  cdleme27N  40370  cdleme30a  40379  cdleme35fnpq  40450  cdleme35b  40451  cdleme35c  40452  cdleme42h  40483  cdleme42i  40484  cdleme48bw  40503  cdlemg2fv2  40601  cdlemg7fvbwN  40608  cdlemg8b  40629  cdlemg11b  40643  trlcolem  40727  trljco  40741  cdlemi1  40819  cdlemk48  40951  cdlemn2  41196  dihjustlem  41217  dihord1  41219  dihord5apre  41263  dihglbcpreN  41301  dihmeetlem3N  41306  dihmeetlem11N  41318