Theorem latlej1 17060

Description: A join's first argument is less than or equal to the join. (chub1 28366 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 1061	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat)
5		simp2 1062	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵)
6		simp3 1063	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵)
7		eqid 2622	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
8	1, 3, 7, 4, 5, 6	latcl2 17048	. . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
9	8	simpld 475	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
10	1, 2, 3, 4, 5, 6, 9	lejoin1 17012	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ≤ (𝑋 ∨ 𝑌))

Syntax hints:   → wi 4   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990  ⟨cop 4183   class class class wbr 4653  dom cdm 5114  ‘cfv 5888  (class class class)co 6650  Basecbs 15857  lecple 15948  joincjn 16944  meetcmee 16945  Latclat 17045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-lub 16974  df-join 16976  df-lat 17046

This theorem is referenced by:  latjlej1  17065  latnlej  17068  latnlej2  17071  latjidm  17074  latnle  17085  latabs2  17088  latmlej11  17090  latjass  17095  mod1ile  17105  lubun  17123  oldmm1  34504  olj01  34512  omllaw5N  34534  cvlexchb1  34617  cvlsupr2  34630  cvlsupr7  34635  hlatlej1  34661  hlrelat5N  34687  2atjm  34731  2llnmj  34846  lplnexllnN  34850  2llnjaN  34852  2llnm2N  34854  4atlem3a  34883  2lplnja  34905  2lplnm2N  34907  2lplnmj  34908  dalemply  34940  dalemsly  34941  dalem10  34959  dalem13  34962  dalem21  34980  dalem55  35013  2llnma1b  35072  cdlema1N  35077  elpaddn0  35086  paddasslem12  35117  paddasslem13  35118  pmapjoin  35138  dalawlem2  35158  dalawlem7  35163  dalawlem11  35167  dalawlem12  35168  lhpmcvr3  35311  lhpmcvr5N  35313  lhpmcvr6N  35314  lautj  35379  trljat1  35453  cdlemc1  35478  cdlemc4  35481  cdleme1  35514  cdleme8  35537  cdleme11g  35552  cdleme22e  35632  cdleme22eALTN  35633  cdleme23b  35638  cdleme23c  35639  cdleme27N  35657  cdleme30a  35666  cdleme35fnpq  35737  cdleme35b  35738  cdleme35c  35739  cdleme42h  35770  cdleme42i  35771  cdleme48bw  35790  cdlemg2fv2  35888  cdlemg7fvbwN  35895  cdlemg8b  35916  cdlemg11b  35930  trlcolem  36014  trljco  36028  cdlemi1  36106  cdlemk48  36238  cdlemn2  36484  dihjustlem  36505  dihord1  36507  dihord5apre  36551  dihglbcpreN  36589  dihmeetlem3N  36594  dihmeetlem11N  36606