Theorem latlej1 17265

Description: A join's first argument is less than or equal to the join. (chub1 28694 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 1159	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat)
5		simp2 1160	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵)
6		simp3 1161	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵)
7		eqid 2806	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
8	1, 3, 7, 4, 5, 6	latcl2 17253	. . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
9	8	simpld 484	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
10	1, 2, 3, 4, 5, 6, 9	lejoin1 17217	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ≤ (𝑋 ∨ 𝑌))

Syntax hints:   → wi 4   ∧ w3a 1100   = wceq 1637   ∈ wcel 2156  ⟨cop 4376   class class class wbr 4844  dom cdm 5311  ‘cfv 6101  (class class class)co 6874  Basecbs 16068  lecple 16160  joincjn 17149  meetcmee 17150  Latclat 17250

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-riota 6835  df-ov 6877  df-oprab 6878  df-lub 17179  df-join 17181  df-lat 17251

This theorem is referenced by:  latjlej1  17270  latnlej  17273  latnlej2  17276  latjidm  17279  latnle  17290  latabs2  17293  latmlej11  17295  latjass  17300  mod1ile  17310  lubun  17328  oldmm1  34997  olj01  35005  omllaw5N  35027  cvlexchb1  35110  cvlsupr2  35123  cvlsupr7  35128  hlatlej1  35155  hlrelat5N  35181  2atjm  35225  2llnmj  35340  lplnexllnN  35344  2llnjaN  35346  2llnm2N  35348  4atlem3a  35377  2lplnja  35399  2lplnm2N  35401  2lplnmj  35402  dalemply  35434  dalemsly  35435  dalem10  35453  dalem13  35456  dalem21  35474  dalem55  35507  2llnma1b  35566  cdlema1N  35571  elpaddn0  35580  paddasslem12  35611  paddasslem13  35612  pmapjoin  35632  dalawlem2  35652  dalawlem7  35657  dalawlem11  35661  dalawlem12  35662  lhpmcvr3  35805  lhpmcvr5N  35807  lhpmcvr6N  35808  lautj  35873  trljat1  35947  cdlemc1  35972  cdlemc4  35975  cdleme1  36008  cdleme8  36031  cdleme11g  36046  cdleme22e  36125  cdleme22eALTN  36126  cdleme23b  36131  cdleme23c  36132  cdleme27N  36150  cdleme30a  36159  cdleme35fnpq  36230  cdleme35b  36231  cdleme35c  36232  cdleme42h  36263  cdleme42i  36264  cdleme48bw  36283  cdlemg2fv2  36381  cdlemg7fvbwN  36388  cdlemg8b  36409  cdlemg11b  36423  trlcolem  36507  trljco  36521  cdlemi1  36599  cdlemk48  36731  cdlemn2  36976  dihjustlem  36997  dihord1  36999  dihord5apre  37043  dihglbcpreN  37081  dihmeetlem3N  37086  dihmeetlem11N  37098