![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > latjle12 | Structured version Visualization version GIF version |
Description: A join is less than or equal to a third value iff each argument is less than or equal to the third value. (chlub 31271 analog.) (Contributed by NM, 17-Sep-2011.) |
Ref | Expression |
---|---|
latlej.b | β’ π΅ = (BaseβπΎ) |
latlej.l | β’ β€ = (leβπΎ) |
latlej.j | β’ β¨ = (joinβπΎ) |
Ref | Expression |
---|---|
latjle12 | β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ π β§ π β€ π) β (π β¨ π) β€ π)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | latlej.b | . 2 β’ π΅ = (BaseβπΎ) | |
2 | latlej.l | . 2 β’ β€ = (leβπΎ) | |
3 | latlej.j | . 2 β’ β¨ = (joinβπΎ) | |
4 | latpos 18403 | . . 3 β’ (πΎ β Lat β πΎ β Poset) | |
5 | 4 | adantr 480 | . 2 β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β πΎ β Poset) |
6 | simpr1 1191 | . 2 β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) | |
7 | simpr2 1192 | . 2 β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) | |
8 | simpr3 1193 | . 2 β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) | |
9 | eqid 2726 | . . . 4 β’ (meetβπΎ) = (meetβπΎ) | |
10 | simpl 482 | . . . 4 β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β πΎ β Lat) | |
11 | 1, 3, 9, 10, 6, 7 | latcl2 18401 | . . 3 β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (β¨π, πβ© β dom β¨ β§ β¨π, πβ© β dom (meetβπΎ))) |
12 | 11 | simpld 494 | . 2 β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β β¨π, πβ© β dom β¨ ) |
13 | 1, 2, 3, 5, 6, 7, 8, 12 | joinle 18351 | 1 β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ π β§ π β€ π) β (π β¨ π) β€ π)) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β wb 205 β§ wa 395 β§ w3a 1084 = wceq 1533 β wcel 2098 β¨cop 4629 class class class wbr 5141 dom cdm 5669 βcfv 6537 (class class class)co 7405 Basecbs 17153 lecple 17213 Posetcpo 18272 joincjn 18276 meetcmee 18277 Latclat 18396 |
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 2697 ax-rep 5278 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7722 |
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 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-nfc 2879 df-ne 2935 df-ral 3056 df-rex 3065 df-rmo 3370 df-reu 3371 df-rab 3427 df-v 3470 df-sbc 3773 df-csb 3889 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-nul 4318 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-iun 4992 df-br 5142 df-opab 5204 df-mpt 5225 df-id 5567 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-iota 6489 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7361 df-ov 7408 df-oprab 7409 df-poset 18278 df-lub 18311 df-join 18313 df-lat 18397 |
This theorem is referenced by: latleeqj1 18416 latjlej1 18418 latjidm 18427 latledi 18442 latjass 18448 mod1ile 18458 lubun 18480 oldmm1 38600 olj01 38608 cvlexchb1 38713 cvlcvr1 38722 hlrelat 38786 hlrelat2 38787 exatleN 38788 hlrelat3 38796 cvrexchlem 38803 cvratlem 38805 cvrat 38806 atlelt 38822 ps-1 38861 hlatexch3N 38864 hlatexch4 38865 3atlem1 38867 3atlem2 38868 lplnexllnN 38948 2llnjaN 38950 4atlem3 38980 4atlem10 38990 4atlem11b 38992 4atlem11 38993 4atlem12b 38995 4atlem12 38996 2lplnja 39003 dalem1 39043 dalem3 39048 dalem8 39054 dalem16 39063 dalem17 39064 dalem21 39078 dalem25 39082 dalem39 39095 dalem54 39110 dalem60 39116 linepsubN 39136 pmapsub 39152 lneq2at 39162 2llnma3r 39172 cdlema1N 39175 cdlemblem 39177 paddasslem5 39208 paddasslem12 39215 paddasslem13 39216 llnexchb2 39253 dalawlem3 39257 dalawlem5 39259 dalawlem8 39262 dalawlem11 39265 dalawlem12 39266 lhp2lt 39385 lhpexle2lem 39393 lhpexle3lem 39395 4atexlemtlw 39451 4atexlemnclw 39454 lautj 39477 cdlemd3 39584 cdleme3g 39618 cdleme3h 39619 cdleme7d 39630 cdleme11c 39645 cdleme15d 39661 cdleme17b 39671 cdleme19a 39687 cdleme20j 39702 cdleme21c 39711 cdleme22b 39725 cdleme22d 39727 cdleme28a 39754 cdleme35a 39832 cdleme35fnpq 39833 cdleme35b 39834 cdleme35f 39838 cdleme42c 39856 cdleme42i 39867 cdlemf1 39945 cdlemg4c 39996 cdlemg6c 40004 cdlemg8b 40012 cdlemg10 40025 cdlemg11b 40026 cdlemg13a 40035 cdlemg17a 40045 cdlemg18b 40063 cdlemg27a 40076 cdlemg33b0 40085 cdlemg35 40097 cdlemg42 40113 cdlemg46 40119 trljco 40124 tendopltp 40164 cdlemk3 40217 cdlemk10 40227 cdlemk1u 40243 cdlemk39 40300 dialss 40430 dia2dimlem1 40448 dia2dimlem10 40457 dia2dimlem12 40459 cdlemm10N 40502 djajN 40521 diblss 40554 cdlemn2 40579 dihord2pre2 40610 dib2dim 40627 dih2dimb 40628 dih2dimbALTN 40629 dihmeetlem6 40693 dihjatcclem1 40802 |
Copyright terms: Public domain | W3C validator |