Theorem latlej1 18385

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ⟨cop 4588   class class class wbr 5100  dom cdm 5634  ‘cfv 6502  (class class class)co 7370  Basecbs 17150  lecple 17198  joincjn 18248  meetcmee 18249  Latclat 18368

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 2185  ax-ext 2709  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-riota 7327  df-ov 7373  df-oprab 7374  df-lub 18281  df-join 18283  df-lat 18369

This theorem is referenced by:  latjlej1  18390  latnlej  18393  latnlej2  18396  latjidm  18399  latnle  18410  latabs2  18413  latmlej11  18415  latjass  18420  mod1ile  18430  lubun  18452  oldmm1  39622  olj01  39630  omllaw5N  39652  cvlexchb1  39735  cvlsupr2  39748  cvlsupr7  39753  hlatlej1  39780  hlrelat5N  39806  2atjm  39850  2llnmj  39965  lplnexllnN  39969  2llnjaN  39971  2llnm2N  39973  4atlem3a  40002  2lplnja  40024  2lplnm2N  40026  2lplnmj  40027  dalemply  40059  dalemsly  40060  dalem10  40078  dalem13  40081  dalem21  40099  dalem55  40132  2llnma1b  40191  cdlema1N  40196  elpaddn0  40205  paddasslem12  40236  paddasslem13  40237  pmapjoin  40257  dalawlem2  40277  dalawlem7  40282  dalawlem11  40286  dalawlem12  40287  lhpmcvr3  40430  lhpmcvr5N  40432  lhpmcvr6N  40433  lautj  40498  trljat1  40571  cdlemc1  40596  cdlemc4  40599  cdleme1  40632  cdleme8  40655  cdleme11g  40670  cdleme22e  40749  cdleme22eALTN  40750  cdleme23b  40755  cdleme23c  40756  cdleme27N  40774  cdleme30a  40783  cdleme35fnpq  40854  cdleme35b  40855  cdleme35c  40856  cdleme42h  40887  cdleme42i  40888  cdleme48bw  40907  cdlemg2fv2  41005  cdlemg7fvbwN  41012  cdlemg8b  41033  cdlemg11b  41047  trlcolem  41131  trljco  41145  cdlemi1  41223  cdlemk48  41355  cdlemn2  41600  dihjustlem  41621  dihord1  41623  dihord5apre  41667  dihglbcpreN  41705  dihmeetlem3N  41710  dihmeetlem11N  41722