![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > latmle2 | Structured version Visualization version GIF version |
Description: A meet is less than or equal to its second argument. (Contributed by NM, 21-Oct-2011.) |
Ref | Expression |
---|---|
latmle.b | ⊢ 𝐵 = (Base‘𝐾) |
latmle.l | ⊢ ≤ = (le‘𝐾) |
latmle.m | ⊢ ∧ = (meet‘𝐾) |
Ref | Expression |
---|---|
latmle2 | ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌) |
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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |