Theorem latmle2 17971

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 1138	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat)
5		simp2 1139	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵)
6		simp3 1140	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵)
7		eqid 2737	. . . 4 ⊢ (join‘𝐾) = (join‘𝐾)
8	1, 7, 3, 4, 5, 6	latcl2 17942	. . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom (join‘𝐾) ∧ ⟨𝑋, 𝑌⟩ ∈ dom ∧ ))
9	8	simprd 499	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )
10	1, 2, 3, 4, 5, 6, 9	lemeet2 17905	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌)

Syntax hints:   → wi 4   ∧ w3a 1089   = wceq 1543   ∈ wcel 2110  ⟨cop 4547   class class class wbr 5053  dom cdm 5551  ‘cfv 6380  (class class class)co 7213  Basecbs 16760  lecple 16809  joincjn 17818  meetcmee 17819  Latclat 17937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-glb 17853  df-meet 17855  df-lat 17938

This theorem is referenced by:  latmlem1  17975  latledi  17983  mod1ile  17999  oldmm1  36968  olm01  36987  cmtcomlemN  36999  cmtbr4N  37006  meetat  37047  cvrexchlem  37170  cvrat4  37194  2llnmj  37311  2lplnmj  37373  dalem25  37449  dalem54  37477  dalem57  37480  cdlema1N  37542  cdlemb  37545  llnexchb2lem  37619  llnexch2N  37621  dalawlem1  37622  dalawlem3  37624  pl42lem1N  37730  lhpelim  37788  lhpat3  37797  4atexlemunv  37817  4atexlemtlw  37818  4atexlemnclw  37821  4atexlemex2  37822  lautm  37845  trlle  37935  cdlemc2  37943  cdlemc5  37946  cdlemd2  37950  cdleme0b  37963  cdleme0c  37964  cdleme0fN  37969  cdleme01N  37972  cdleme0ex1N  37974  cdleme2  37979  cdleme3b  37980  cdleme3c  37981  cdleme3g  37985  cdleme3h  37986  cdleme7aa  37993  cdleme7c  37996  cdleme7d  37997  cdleme7e  37998  cdleme7ga  37999  cdleme11fN  38015  cdleme11k  38019  cdleme15d  38028  cdleme16f  38034  cdlemednpq  38050  cdleme19c  38056  cdleme20aN  38060  cdleme20c  38062  cdleme20j  38069  cdleme21c  38078  cdleme21ct  38080  cdleme22cN  38093  cdleme22f  38097  cdleme23a  38100  cdleme28a  38121  cdleme35d  38203  cdleme35f  38205  cdlemeg46frv  38276  cdlemeg46rgv  38279  cdlemeg46req  38280  cdlemg2fv2  38351  cdlemg2m  38355  cdlemg4  38368  cdlemg10bALTN  38387  cdlemg31b  38449  trlcolem  38477  cdlemk14  38605  dia2dimlem1  38815  docaclN  38875  doca2N  38877  djajN  38888  dihjustlem  38967  dihord1  38969  dihord2a  38970  dihord2b  38971  dihord2cN  38972  dihord11b  38973  dihord11c  38975  dihord2pre  38976  dihlsscpre  38985  dihvalcq2  38998  dihopelvalcpre  38999  dihord6apre  39007  dihord5b  39010  dihord5apre  39013  dihmeetlem1N  39041  dihglblem5apreN  39042  dihglblem3N  39046  dihmeetbclemN  39055  dihmeetlem4preN  39057  dihmeetlem7N  39061  dihmeetlem9N  39066  dihjatcclem4  39172