Theorem latmle2 18366

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

Hypotheses

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

Assertion

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

Proof of Theorem latmle2

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 2731	. . . 4 ⊢ (join‘𝐾) = (join‘𝐾)
8	1, 7, 3, 4, 5, 6	latcl2 18337	. . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom (join‘𝐾) ∧ ⟨𝑋, 𝑌⟩ ∈ dom ∧ ))
9	8	simprd 495	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )
10	1, 2, 3, 4, 5, 6, 9	lemeet2 18298	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌)

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111  ⟨cop 4577   class class class wbr 5086  dom cdm 5611  ‘cfv 6476  (class class class)co 7341  Basecbs 17115  lecple 17163  joincjn 18212  meetcmee 18213  Latclat 18332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5212  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-riota 7298  df-ov 7344  df-oprab 7345  df-glb 18246  df-meet 18248  df-lat 18333

This theorem is referenced by:  latmlem1  18370  latledi  18378  mod1ile  18394  oldmm1  39256  olm01  39275  cmtcomlemN  39287  cmtbr4N  39294  meetat  39335  cvrexchlem  39458  cvrat4  39482  2llnmj  39599  2lplnmj  39661  dalem25  39737  dalem54  39765  dalem57  39768  cdlema1N  39830  cdlemb  39833  llnexchb2lem  39907  llnexch2N  39909  dalawlem1  39910  dalawlem3  39912  pl42lem1N  40018  lhpelim  40076  lhpat3  40085  4atexlemunv  40105  4atexlemtlw  40106  4atexlemnclw  40109  4atexlemex2  40110  lautm  40133  trlle  40223  cdlemc2  40231  cdlemc5  40234  cdlemd2  40238  cdleme0b  40251  cdleme0c  40252  cdleme0fN  40257  cdleme01N  40260  cdleme0ex1N  40262  cdleme2  40267  cdleme3b  40268  cdleme3c  40269  cdleme3g  40273  cdleme3h  40274  cdleme7aa  40281  cdleme7c  40284  cdleme7d  40285  cdleme7e  40286  cdleme7ga  40287  cdleme11fN  40303  cdleme11k  40307  cdleme15d  40316  cdleme16f  40322  cdlemednpq  40338  cdleme19c  40344  cdleme20aN  40348  cdleme20c  40350  cdleme20j  40357  cdleme21c  40366  cdleme21ct  40368  cdleme22cN  40381  cdleme22f  40385  cdleme23a  40388  cdleme28a  40409  cdleme35d  40491  cdleme35f  40493  cdlemeg46frv  40564  cdlemeg46rgv  40567  cdlemeg46req  40568  cdlemg2fv2  40639  cdlemg2m  40643  cdlemg4  40656  cdlemg10bALTN  40675  cdlemg31b  40737  trlcolem  40765  cdlemk14  40893  dia2dimlem1  41103  docaclN  41163  doca2N  41165  djajN  41176  dihjustlem  41255  dihord1  41257  dihord2a  41258  dihord2b  41259  dihord2cN  41260  dihord11b  41261  dihord11c  41263  dihord2pre  41264  dihlsscpre  41273  dihvalcq2  41286  dihopelvalcpre  41287  dihord6apre  41295  dihord5b  41298  dihord5apre  41301  dihmeetlem1N  41329  dihglblem5apreN  41330  dihglblem3N  41334  dihmeetbclemN  41343  dihmeetlem4preN  41345  dihmeetlem7N  41349  dihmeetlem9N  41354  dihjatcclem4  41460