Nearby theorems
|
|
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 1133 | . 2 β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β πΎ β Lat) | |
| 5 | simp2 1134 | . 2 β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β π β π΅) | |
| 6 | simp3 1135 | . 2 β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β π β π΅) | |
| 7 | eqid 2724 | . . . 4 β’ (joinβπΎ) = (joinβπΎ) | |
| 8 | 1, 7, 3, 4, 5, 6 | latcl2 18388 | . . 3 β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (β¨π, πβ© β dom (joinβπΎ) β§ β¨π, πβ© β dom β§ )) |
| 9 | 8 | simprd 495 | . 2 β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β β¨π, πβ© β dom β§ ) |
| 10 | 1, 2, 3, 4, 5, 6, 9 | lemeet2 18351 | 1 β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β€ π) |
| Colors of variables: wff setvar class |
| Syntax hints: β wi 4 β§ w3a 1084 = wceq 1533 β wcel 2098 β¨cop 4626 class class class wbr 5138 dom cdm 5666 βcfv 6533 (class class class)co 7401 Basecbs 17140 lecple 17200 joincjn 18263 meetcmee 18264 Latclat 18383 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-rep 5275 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7718 |
| This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-ral 3054 df-rex 3063 df-rmo 3368 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-iun 4989 df-br 5139 df-opab 5201 df-mpt 5222 df-id 5564 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7357 df-ov 7404 df-oprab 7405 df-glb 18299 df-meet 18301 df-lat 18384 |
| This theorem is referenced by: latmlem1 18421 latledi 18429 mod1ile 18445 oldmm1 38543 olm01 38562 cmtcomlemN 38574 cmtbr4N 38581 meetat 38622 cvrexchlem 38746 cvrat4 38770 2llnmj 38887 2lplnmj 38949 dalem25 39025 dalem54 39053 dalem57 39056 cdlema1N 39118 cdlemb 39121 llnexchb2lem 39195 llnexch2N 39197 dalawlem1 39198 dalawlem3 39200 pl42lem1N 39306 lhpelim 39364 lhpat3 39373 4atexlemunv 39393 4atexlemtlw 39394 4atexlemnclw 39397 4atexlemex2 39398 lautm 39421 trlle 39511 cdlemc2 39519 cdlemc5 39522 cdlemd2 39526 cdleme0b 39539 cdleme0c 39540 cdleme0fN 39545 cdleme01N 39548 cdleme0ex1N 39550 cdleme2 39555 cdleme3b 39556 cdleme3c 39557 cdleme3g 39561 cdleme3h 39562 cdleme7aa 39569 cdleme7c 39572 cdleme7d 39573 cdleme7e 39574 cdleme7ga 39575 cdleme11fN 39591 cdleme11k 39595 cdleme15d 39604 cdleme16f 39610 cdlemednpq 39626 cdleme19c 39632 cdleme20aN 39636 cdleme20c 39638 cdleme20j 39645 cdleme21c 39654 cdleme21ct 39656 cdleme22cN 39669 cdleme22f 39673 cdleme23a 39676 cdleme28a 39697 cdleme35d 39779 cdleme35f 39781 cdlemeg46frv 39852 cdlemeg46rgv 39855 cdlemeg46req 39856 cdlemg2fv2 39927 cdlemg2m 39931 cdlemg4 39944 cdlemg10bALTN 39963 cdlemg31b 40025 trlcolem 40053 cdlemk14 40181 dia2dimlem1 40391 docaclN 40451 doca2N 40453 djajN 40464 dihjustlem 40543 dihord1 40545 dihord2a 40546 dihord2b 40547 dihord2cN 40548 dihord11b 40549 dihord11c 40551 dihord2pre 40552 dihlsscpre 40561 dihvalcq2 40574 dihopelvalcpre 40575 dihord6apre 40583 dihord5b 40586 dihord5apre 40589 dihmeetlem1N 40617 dihglblem5apreN 40618 dihglblem3N 40622 dihmeetbclemN 40631 dihmeetlem4preN 40633 dihmeetlem7N 40637 dihmeetlem9N 40642 dihjatcclem4 40748 |
| Copyright terms: Public domain | W3C validator |