Theorem latmle2 18379

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ⟨cop 4583   class class class wbr 5095  dom cdm 5621  ‘cfv 6489  (class class class)co 7355  Basecbs 17127  lecple 17175  joincjn 18225  meetcmee 18226  Latclat 18345

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rmo 3347  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7312  df-ov 7358  df-oprab 7359  df-glb 18259  df-meet 18261  df-lat 18346

This theorem is referenced by:  latmlem1  18383  latledi  18391  mod1ile  18407  oldmm1  39389  olm01  39408  cmtcomlemN  39420  cmtbr4N  39427  meetat  39468  cvrexchlem  39591  cvrat4  39615  2llnmj  39732  2lplnmj  39794  dalem25  39870  dalem54  39898  dalem57  39901  cdlema1N  39963  cdlemb  39966  llnexchb2lem  40040  llnexch2N  40042  dalawlem1  40043  dalawlem3  40045  pl42lem1N  40151  lhpelim  40209  lhpat3  40218  4atexlemunv  40238  4atexlemtlw  40239  4atexlemnclw  40242  4atexlemex2  40243  lautm  40266  trlle  40356  cdlemc2  40364  cdlemc5  40367  cdlemd2  40371  cdleme0b  40384  cdleme0c  40385  cdleme0fN  40390  cdleme01N  40393  cdleme0ex1N  40395  cdleme2  40400  cdleme3b  40401  cdleme3c  40402  cdleme3g  40406  cdleme3h  40407  cdleme7aa  40414  cdleme7c  40417  cdleme7d  40418  cdleme7e  40419  cdleme7ga  40420  cdleme11fN  40436  cdleme11k  40440  cdleme15d  40449  cdleme16f  40455  cdlemednpq  40471  cdleme19c  40477  cdleme20aN  40481  cdleme20c  40483  cdleme20j  40490  cdleme21c  40499  cdleme21ct  40501  cdleme22cN  40514  cdleme22f  40518  cdleme23a  40521  cdleme28a  40542  cdleme35d  40624  cdleme35f  40626  cdlemeg46frv  40697  cdlemeg46rgv  40700  cdlemeg46req  40701  cdlemg2fv2  40772  cdlemg2m  40776  cdlemg4  40789  cdlemg10bALTN  40808  cdlemg31b  40870  trlcolem  40898  cdlemk14  41026  dia2dimlem1  41236  docaclN  41296  doca2N  41298  djajN  41309  dihjustlem  41388  dihord1  41390  dihord2a  41391  dihord2b  41392  dihord2cN  41393  dihord11b  41394  dihord11c  41396  dihord2pre  41397  dihlsscpre  41406  dihvalcq2  41419  dihopelvalcpre  41420  dihord6apre  41428  dihord5b  41431  dihord5apre  41434  dihmeetlem1N  41462  dihglblem5apreN  41463  dihglblem3N  41467  dihmeetbclemN  41476  dihmeetlem4preN  41478  dihmeetlem7N  41482  dihmeetlem9N  41487  dihjatcclem4  41593