Theorem latlej1 18518

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  ⟨cop 4654   class class class wbr 5166  dom cdm 5700  ‘cfv 6573  (class class class)co 7448  Basecbs 17258  lecple 17318  joincjn 18381  meetcmee 18382  Latclat 18501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-lub 18416  df-join 18418  df-lat 18502

This theorem is referenced by:  latjlej1  18523  latnlej  18526  latnlej2  18529  latjidm  18532  latnle  18543  latabs2  18546  latmlej11  18548  latjass  18553  mod1ile  18563  lubun  18585  oldmm1  39173  olj01  39181  omllaw5N  39203  cvlexchb1  39286  cvlsupr2  39299  cvlsupr7  39304  hlatlej1  39331  hlrelat5N  39358  2atjm  39402  2llnmj  39517  lplnexllnN  39521  2llnjaN  39523  2llnm2N  39525  4atlem3a  39554  2lplnja  39576  2lplnm2N  39578  2lplnmj  39579  dalemply  39611  dalemsly  39612  dalem10  39630  dalem13  39633  dalem21  39651  dalem55  39684  2llnma1b  39743  cdlema1N  39748  elpaddn0  39757  paddasslem12  39788  paddasslem13  39789  pmapjoin  39809  dalawlem2  39829  dalawlem7  39834  dalawlem11  39838  dalawlem12  39839  lhpmcvr3  39982  lhpmcvr5N  39984  lhpmcvr6N  39985  lautj  40050  trljat1  40123  cdlemc1  40148  cdlemc4  40151  cdleme1  40184  cdleme8  40207  cdleme11g  40222  cdleme22e  40301  cdleme22eALTN  40302  cdleme23b  40307  cdleme23c  40308  cdleme27N  40326  cdleme30a  40335  cdleme35fnpq  40406  cdleme35b  40407  cdleme35c  40408  cdleme42h  40439  cdleme42i  40440  cdleme48bw  40459  cdlemg2fv2  40557  cdlemg7fvbwN  40564  cdlemg8b  40585  cdlemg11b  40599  trlcolem  40683  trljco  40697  cdlemi1  40775  cdlemk48  40907  cdlemn2  41152  dihjustlem  41173  dihord1  41175  dihord5apre  41219  dihglbcpreN  41257  dihmeetlem3N  41262  dihmeetlem11N  41274