Theorem latmle2 18632

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 1154	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat)
5		simp2 1155	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵)
6		simp3 1156	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵)
7		eqid 2761	. . . 4 ⊢ (join‘𝐾) = (join‘𝐾)
8	1, 7, 3, 4, 5, 6	latcl2 18603	. . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom (join‘𝐾) ∧ ⟨𝑋, 𝑌⟩ ∈ dom ∧ ))
9	8	simprd 501	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )
10	1, 2, 3, 4, 5, 6, 9	lemeet2 18564	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ⟨cop 4590   class class class wbr 5103  dom cdm 5651  ‘cfv 6537  (class class class)co 7418  Basecbs 17380  lecple 17428  joincjn 18478  meetcmee 18479  Latclat 18598

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-glb 18512  df-meet 18514  df-lat 18599

This theorem is used by:  latmlem1  18636  latledi  18644  mod1ile  18660  oldmm1  40254  olm01  40273  cmtcomlemN  40285  cmtbr4N  40292  meetat  40333  cvrexchlem  40456  cvrat4  40480  2llnmj  40597  2lplnmj  40659  dalem25  40735  dalem54  40763  dalem57  40766  cdlema1N  40828  cdlemb  40831  llnexchb2lem  40905  llnexch2N  40907  dalawlem1  40908  dalawlem3  40910  pl42lem1N  41016  lhpelim  41074  lhpat3  41083  4atexlemunv  41103  4atexlemtlw  41104  4atexlemnclw  41107  4atexlemex2  41108  lautm  41131  trlle  41221  cdlemc2  41229  cdlemc5  41232  cdlemd2  41236  cdleme0b  41249  cdleme0c  41250  cdleme0fN  41255  cdleme01N  41258  cdleme0ex1N  41260  cdleme2  41265  cdleme3b  41266  cdleme3c  41267  cdleme3g  41271  cdleme3h  41272  cdleme7aa  41279  cdleme7c  41282  cdleme7d  41283  cdleme7e  41284  cdleme7ga  41285  cdleme11fN  41301  cdleme11k  41305  cdleme15d  41314  cdleme16f  41320  cdlemednpq  41336  cdleme19c  41342  cdleme20aN  41346  cdleme20c  41348  cdleme20j  41355  cdleme21c  41364  cdleme21ct  41366  cdleme22cN  41379  cdleme22f  41383  cdleme23a  41386  cdleme28a  41407  cdleme35d  41489  cdleme35f  41491  cdlemeg46frv  41562  cdlemeg46rgv  41565  cdlemeg46req  41566  cdlemg2fv2  41637  cdlemg2m  41641  cdlemg4  41654  cdlemg10bALTN  41673  cdlemg31b  41735  trlcolem  41763  cdlemk14  41891  dia2dimlem1  42101  docaclN  42161  doca2N  42163  djajN  42174  dihjustlem  42253  dihord1  42255  dihord2a  42256  dihord2b  42257  dihord2cN  42258  dihord11b  42259  dihord11c  42261  dihord2pre  42262  dihlsscpre  42271  dihvalcq2  42284  dihopelvalcpre  42285  dihord6apre  42293  dihord5b  42296  dihord5apre  42299  dihmeetlem1N  42327  dihglblem5apreN  42328  dihglblem3N  42332  dihmeetbclemN  42341  dihmeetlem4preN  42343  dihmeetlem7N  42347  dihmeetlem9N  42352  dihjatcclem4  42458