Theorem latmle2 18098

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 1134	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat)
5		simp2 1135	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵)
6		simp3 1136	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵)
7		eqid 2738	. . . 4 ⊢ (join‘𝐾) = (join‘𝐾)
8	1, 7, 3, 4, 5, 6	latcl2 18069	. . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom (join‘𝐾) ∧ ⟨𝑋, 𝑌⟩ ∈ dom ∧ ))
9	8	simprd 495	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )
10	1, 2, 3, 4, 5, 6, 9	lemeet2 18032	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌)

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  ⟨cop 4564   class class class wbr 5070  dom cdm 5580  ‘cfv 6418  (class class class)co 7255  Basecbs 16840  lecple 16895  joincjn 17944  meetcmee 17945  Latclat 18064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-glb 17980  df-meet 17982  df-lat 18065

This theorem is referenced by:  latmlem1  18102  latledi  18110  mod1ile  18126  oldmm1  37158  olm01  37177  cmtcomlemN  37189  cmtbr4N  37196  meetat  37237  cvrexchlem  37360  cvrat4  37384  2llnmj  37501  2lplnmj  37563  dalem25  37639  dalem54  37667  dalem57  37670  cdlema1N  37732  cdlemb  37735  llnexchb2lem  37809  llnexch2N  37811  dalawlem1  37812  dalawlem3  37814  pl42lem1N  37920  lhpelim  37978  lhpat3  37987  4atexlemunv  38007  4atexlemtlw  38008  4atexlemnclw  38011  4atexlemex2  38012  lautm  38035  trlle  38125  cdlemc2  38133  cdlemc5  38136  cdlemd2  38140  cdleme0b  38153  cdleme0c  38154  cdleme0fN  38159  cdleme01N  38162  cdleme0ex1N  38164  cdleme2  38169  cdleme3b  38170  cdleme3c  38171  cdleme3g  38175  cdleme3h  38176  cdleme7aa  38183  cdleme7c  38186  cdleme7d  38187  cdleme7e  38188  cdleme7ga  38189  cdleme11fN  38205  cdleme11k  38209  cdleme15d  38218  cdleme16f  38224  cdlemednpq  38240  cdleme19c  38246  cdleme20aN  38250  cdleme20c  38252  cdleme20j  38259  cdleme21c  38268  cdleme21ct  38270  cdleme22cN  38283  cdleme22f  38287  cdleme23a  38290  cdleme28a  38311  cdleme35d  38393  cdleme35f  38395  cdlemeg46frv  38466  cdlemeg46rgv  38469  cdlemeg46req  38470  cdlemg2fv2  38541  cdlemg2m  38545  cdlemg4  38558  cdlemg10bALTN  38577  cdlemg31b  38639  trlcolem  38667  cdlemk14  38795  dia2dimlem1  39005  docaclN  39065  doca2N  39067  djajN  39078  dihjustlem  39157  dihord1  39159  dihord2a  39160  dihord2b  39161  dihord2cN  39162  dihord11b  39163  dihord11c  39165  dihord2pre  39166  dihlsscpre  39175  dihvalcq2  39188  dihopelvalcpre  39189  dihord6apre  39197  dihord5b  39200  dihord5apre  39203  dihmeetlem1N  39231  dihglblem5apreN  39232  dihglblem3N  39236  dihmeetbclemN  39245  dihmeetlem4preN  39247  dihmeetlem7N  39251  dihmeetlem9N  39256  dihjatcclem4  39362