Theorem latmle2 18428

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  ⟨cop 4634   class class class wbr 5148  dom cdm 5676  ‘cfv 6543  (class class class)co 7412  Basecbs 17151  lecple 17211  joincjn 18274  meetcmee 18275  Latclat 18394

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-glb 18310  df-meet 18312  df-lat 18395

This theorem is referenced by:  latmlem1  18432  latledi  18440  mod1ile  18456  oldmm1  38550  olm01  38569  cmtcomlemN  38581  cmtbr4N  38588  meetat  38629  cvrexchlem  38753  cvrat4  38777  2llnmj  38894  2lplnmj  38956  dalem25  39032  dalem54  39060  dalem57  39063  cdlema1N  39125  cdlemb  39128  llnexchb2lem  39202  llnexch2N  39204  dalawlem1  39205  dalawlem3  39207  pl42lem1N  39313  lhpelim  39371  lhpat3  39380  4atexlemunv  39400  4atexlemtlw  39401  4atexlemnclw  39404  4atexlemex2  39405  lautm  39428  trlle  39518  cdlemc2  39526  cdlemc5  39529  cdlemd2  39533  cdleme0b  39546  cdleme0c  39547  cdleme0fN  39552  cdleme01N  39555  cdleme0ex1N  39557  cdleme2  39562  cdleme3b  39563  cdleme3c  39564  cdleme3g  39568  cdleme3h  39569  cdleme7aa  39576  cdleme7c  39579  cdleme7d  39580  cdleme7e  39581  cdleme7ga  39582  cdleme11fN  39598  cdleme11k  39602  cdleme15d  39611  cdleme16f  39617  cdlemednpq  39633  cdleme19c  39639  cdleme20aN  39643  cdleme20c  39645  cdleme20j  39652  cdleme21c  39661  cdleme21ct  39663  cdleme22cN  39676  cdleme22f  39680  cdleme23a  39683  cdleme28a  39704  cdleme35d  39786  cdleme35f  39788  cdlemeg46frv  39859  cdlemeg46rgv  39862  cdlemeg46req  39863  cdlemg2fv2  39934  cdlemg2m  39938  cdlemg4  39951  cdlemg10bALTN  39970  cdlemg31b  40032  trlcolem  40060  cdlemk14  40188  dia2dimlem1  40398  docaclN  40458  doca2N  40460  djajN  40471  dihjustlem  40550  dihord1  40552  dihord2a  40553  dihord2b  40554  dihord2cN  40555  dihord11b  40556  dihord11c  40558  dihord2pre  40559  dihlsscpre  40568  dihvalcq2  40581  dihopelvalcpre  40582  dihord6apre  40590  dihord5b  40593  dihord5apre  40596  dihmeetlem1N  40624  dihglblem5apreN  40625  dihglblem3N  40629  dihmeetbclemN  40638  dihmeetlem4preN  40640  dihmeetlem7N  40644  dihmeetlem9N  40649  dihjatcclem4  40755