Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > latlem12 | Structured version Visualization version GIF version | ||
| Description: An element is less than or equal to a meet iff the element is less than or equal to each argument of the meet. (Contributed by NM, 21-Oct-2011.) |
| Ref | Expression |
|---|---|
| latmle.b | β’ π΅ = (BaseβπΎ) |
| latmle.l | β’ β€ = (leβπΎ) |
| latmle.m | β’ β§ = (meetβπΎ) |
| Ref | Expression |
|---|---|
| latlem12 | β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ π β§ π β€ π) β π β€ (π β§ π))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | latmle.b | . 2 β’ π΅ = (BaseβπΎ) | |
| 2 | latmle.l | . 2 β’ β€ = (leβπΎ) | |
| 3 | latmle.m | . 2 β’ β§ = (meetβπΎ) | |
| 4 | latpos 18396 | . . 3 β’ (πΎ β Lat β πΎ β Poset) | |
| 5 | 4 | adantr 480 | . 2 β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β πΎ β Poset) |
| 6 | simpr2 1194 | . 2 β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) | |
| 7 | simpr3 1195 | . 2 β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) | |
| 8 | simpr1 1193 | . 2 β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) | |
| 9 | eqid 2731 | . . . 4 β’ (joinβπΎ) = (joinβπΎ) | |
| 10 | simpl 482 | . . . 4 β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β πΎ β Lat) | |
| 11 | 1, 9, 3, 10, 6, 7 | latcl2 18394 | . . 3 β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (β¨π, πβ© β dom (joinβπΎ) β§ β¨π, πβ© β dom β§ )) |
| 12 | 11 | simprd 495 | . 2 β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β β¨π, πβ© β dom β§ ) |
| 13 | 1, 2, 3, 5, 6, 7, 8, 12 | meetle 18358 | 1 β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ π β§ π β€ π) β π β€ (π β§ π))) |
| Colors of variables: wff setvar class |
| Syntax hints: β wi 4 β wb 205 β§ wa 395 β§ w3a 1086 = wceq 1540 β wcel 2105 β¨cop 4634 class class class wbr 5148 dom cdm 5676 βcfv 6543 (class class class)co 7412 Basecbs 17149 lecple 17209 Posetcpo 18265 joincjn 18269 meetcmee 18270 Latclat 18389 |
| 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-poset 18271 df-glb 18305 df-meet 18307 df-lat 18390 |
| This theorem is referenced by: latleeqm1 18425 latmlem1 18427 latmidm 18432 latledi 18435 mod1ile 18451 oldmm1 38391 olm01 38410 cmtbr4N 38429 atnle 38491 atlatmstc 38493 hlrelat2 38578 cvrval5 38590 cvrexchlem 38594 2atjm 38620 atbtwn 38621 ps-2b 38657 2atm 38702 2llnm4 38745 2llnmeqat 38746 dalemcea 38835 dalem21 38869 dalem54 38901 dalem55 38902 dalem57 38904 2atm2atN 38960 2llnma1b 38961 cdlemblem 38968 dalawlem2 39047 dalawlem3 39048 dalawlem6 39051 dalawlem11 39056 dalawlem12 39057 lhpocnle 39191 lhpmcvr4N 39201 lhpat3 39221 4atexlemcnd 39247 lautm 39269 trlval3 39362 cdlemc5 39370 cdleme3 39412 cdleme7ga 39423 cdleme7 39424 cdleme11k 39443 cdleme16e 39457 cdleme16f 39458 cdlemednpq 39474 cdleme22aa 39514 cdleme22b 39516 cdleme22cN 39517 cdleme23c 39526 cdlemeg46req 39704 cdlemf2 39737 cdlemg10c 39814 cdlemg12f 39823 cdlemg17dALTN 39839 cdlemg19a 39858 cdlemg27b 39871 cdlemi 39995 cdlemk15 40030 cdlemk50 40127 dia2dimlem1 40239 dihopelvalcpre 40423 dihord5b 40434 dihmeetlem1N 40465 dihglblem5apreN 40466 dihglblem2N 40469 dihmeetlem3N 40480 |
| Copyright terms: Public domain | W3C validator |