Theorem latmle1 18227

Description: A meet is less than or equal to its first argument. (Contributed by NM, 21-Oct-2011.)

Hypotheses

Ref	Expression
latmle.b	⊢ 𝐵 = (Base‘𝐾)
latmle.l	⊢ ≤ = (le‘𝐾)
latmle.m	⊢ ∧ = (meet‘𝐾)

Assertion

Ref	Expression
latmle1	⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑋)

Proof of Theorem latmle1

Step	Hyp	Ref	Expression
1		latmle.b	. 2 ⊢ 𝐵 = (Base‘𝐾)
2		latmle.l	. 2 ⊢ ≤ = (le‘𝐾)
3		latmle.m	. 2 ⊢ ∧ = (meet‘𝐾)
4		simp1 1136	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat)
5		simp2 1137	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵)
6		simp3 1138	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵)
7		eqid 2736	. . . 4 ⊢ (join‘𝐾) = (join‘𝐾)
8	1, 7, 3, 4, 5, 6	latcl2 18199	. . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom (join‘𝐾) ∧ ⟨𝑋, 𝑌⟩ ∈ dom ∧ ))
9	8	simprd 497	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )
10	1, 2, 3, 4, 5, 6, 9	lemeet1 18161	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑋)

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1539   ∈ wcel 2104  ⟨cop 4571   class class class wbr 5081  dom cdm 5600  ‘cfv 6458  (class class class)co 7307  Basecbs 16957  lecple 17014  joincjn 18074  meetcmee 18075  Latclat 18194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-rep 5218  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-riota 7264  df-ov 7310  df-oprab 7311  df-glb 18110  df-meet 18112  df-lat 18195

This theorem is referenced by:  latleeqm1  18230  latmlem1  18232  latnlemlt  18235  latmidm  18237  latabs1  18238  latledi  18240  latmlej11  18241  oldmm1  37273  cmtbr3N  37310  cmtbr4N  37311  lecmtN  37312  cvrat4  37499  2llnmat  37580  llnmlplnN  37595  dalem3  37720  dalem27  37755  dalem54  37782  dalem55  37783  2lnat  37840  cdlema1N  37847  llnexchb2lem  37924  dalawlem1  37927  dalawlem6  37932  dalawlem11  37937  dalawlem12  37938  4atexlemunv  38122  4atexlemc  38125  4atexlemnclw  38126  4atexlemex2  38127  4atexlemcnd  38128  lautm  38150  trlval3  38243  cdlemeulpq  38276  cdleme3h  38291  cdleme4a  38295  cdleme9  38309  cdleme11g  38321  cdleme13  38328  cdleme16e  38338  cdlemednpq  38355  cdleme19b  38360  cdleme20e  38369  cdleme20j  38374  cdleme22cN  38398  cdleme22e  38400  cdleme22eALTN  38401  cdleme22g  38404  cdleme35b  38506  cdleme35f  38510  cdlemeg46vrg  38583  cdlemg11b  38698  cdlemg12f  38704  cdlemg19a  38739  cdlemg31a  38753  cdlemk12  38906  cdlemkole  38909  cdlemk12u  38928  cdlemk37  38970  dia2dimlem1  39120  dihopelvalcpre  39304  dihmeetlem1N  39346  dihglblem5apreN  39347  dihglblem2N  39350  dihmeetlem2N  39355