Theorem latlej1 18403

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ⟨cop 4563   class class class wbr 5074  dom cdm 5620  ‘cfv 6487  (class class class)co 7356  Basecbs 17168  lecple 17216  joincjn 18266  meetcmee 18267  Latclat 18386

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 2184  ax-ext 2707  ax-rep 5201  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7678

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 2931  df-ral 3050  df-rex 3060  df-rmo 3340  df-reu 3341  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-iun 4925  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-riota 7313  df-ov 7359  df-oprab 7360  df-lub 18299  df-join 18301  df-lat 18387

This theorem is referenced by:  latjlej1  18408  latnlej  18411  latnlej2  18414  latjidm  18417  latnle  18428  latabs2  18431  latmlej11  18433  latjass  18438  mod1ile  18448  lubun  18470  oldmm1  39651  olj01  39659  omllaw5N  39681  cvlexchb1  39764  cvlsupr2  39777  cvlsupr7  39782  hlatlej1  39809  hlrelat5N  39835  2atjm  39879  2llnmj  39994  lplnexllnN  39998  2llnjaN  40000  2llnm2N  40002  4atlem3a  40031  2lplnja  40053  2lplnm2N  40055  2lplnmj  40056  dalemply  40088  dalemsly  40089  dalem10  40107  dalem13  40110  dalem21  40128  dalem55  40161  2llnma1b  40220  cdlema1N  40225  elpaddn0  40234  paddasslem12  40265  paddasslem13  40266  pmapjoin  40286  dalawlem2  40306  dalawlem7  40311  dalawlem11  40315  dalawlem12  40316  lhpmcvr3  40459  lhpmcvr5N  40461  lhpmcvr6N  40462  lautj  40527  trljat1  40600  cdlemc1  40625  cdlemc4  40628  cdleme1  40661  cdleme8  40684  cdleme11g  40699  cdleme22e  40778  cdleme22eALTN  40779  cdleme23b  40784  cdleme23c  40785  cdleme27N  40803  cdleme30a  40812  cdleme35fnpq  40883  cdleme35b  40884  cdleme35c  40885  cdleme42h  40916  cdleme42i  40917  cdleme48bw  40936  cdlemg2fv2  41034  cdlemg7fvbwN  41041  cdlemg8b  41062  cdlemg11b  41076  trlcolem  41160  trljco  41174  cdlemi1  41252  cdlemk48  41384  cdlemn2  41629  dihjustlem  41650  dihord1  41652  dihord5apre  41696  dihglbcpreN  41734  dihmeetlem3N  41739  dihmeetlem11N  41751