Theorem latlej1 18373

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ⟨cop 4585   class class class wbr 5097  dom cdm 5623  ‘cfv 6491  (class class class)co 7358  Basecbs 17138  lecple 17186  joincjn 18236  meetcmee 18237  Latclat 18356

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 2183  ax-ext 2707  ax-rep 5223  ax-sep 5240  ax-nul 5250  ax-pow 5309  ax-pr 5376  ax-un 7680

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 2932  df-ral 3051  df-rex 3060  df-rmo 3349  df-reu 3350  df-rab 3399  df-v 3441  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4947  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499  df-riota 7315  df-ov 7361  df-oprab 7362  df-lub 18269  df-join 18271  df-lat 18357

This theorem is referenced by:  latjlej1  18378  latnlej  18381  latnlej2  18384  latjidm  18387  latnle  18398  latabs2  18401  latmlej11  18403  latjass  18408  mod1ile  18418  lubun  18440  oldmm1  39512  olj01  39520  omllaw5N  39542  cvlexchb1  39625  cvlsupr2  39638  cvlsupr7  39643  hlatlej1  39670  hlrelat5N  39696  2atjm  39740  2llnmj  39855  lplnexllnN  39859  2llnjaN  39861  2llnm2N  39863  4atlem3a  39892  2lplnja  39914  2lplnm2N  39916  2lplnmj  39917  dalemply  39949  dalemsly  39950  dalem10  39968  dalem13  39971  dalem21  39989  dalem55  40022  2llnma1b  40081  cdlema1N  40086  elpaddn0  40095  paddasslem12  40126  paddasslem13  40127  pmapjoin  40147  dalawlem2  40167  dalawlem7  40172  dalawlem11  40176  dalawlem12  40177  lhpmcvr3  40320  lhpmcvr5N  40322  lhpmcvr6N  40323  lautj  40388  trljat1  40461  cdlemc1  40486  cdlemc4  40489  cdleme1  40522  cdleme8  40545  cdleme11g  40560  cdleme22e  40639  cdleme22eALTN  40640  cdleme23b  40645  cdleme23c  40646  cdleme27N  40664  cdleme30a  40673  cdleme35fnpq  40744  cdleme35b  40745  cdleme35c  40746  cdleme42h  40777  cdleme42i  40778  cdleme48bw  40797  cdlemg2fv2  40895  cdlemg7fvbwN  40902  cdlemg8b  40923  cdlemg11b  40937  trlcolem  41021  trljco  41035  cdlemi1  41113  cdlemk48  41245  cdlemn2  41490  dihjustlem  41511  dihord1  41513  dihord5apre  41557  dihglbcpreN  41595  dihmeetlem3N  41600  dihmeetlem11N  41612