Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > latjcl | Structured version Visualization version GIF version | ||
| Description: Closure of join operation in a lattice. (chjcom 30746 analog.) (Contributed by NM, 14-Sep-2011.) |
| Ref | Expression |
|---|---|
| latjcl.b | β’ π΅ = (BaseβπΎ) |
| latjcl.j | β’ β¨ = (joinβπΎ) |
| Ref | Expression |
|---|---|
| latjcl | β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | latjcl.b | . . 3 β’ π΅ = (BaseβπΎ) | |
| 2 | latjcl.j | . . 3 β’ β¨ = (joinβπΎ) | |
| 3 | eqid 2732 | . . 3 β’ (meetβπΎ) = (meetβπΎ) | |
| 4 | 1, 2, 3 | latlem 18386 | . 2 β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β ((π β¨ π) β π΅ β§ (π(meetβπΎ)π) β π΅)) |
| 5 | 4 | simpld 495 | 1 β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
| Colors of variables: wff setvar class |
| Syntax hints: β wi 4 β§ w3a 1087 = wceq 1541 β wcel 2106 βcfv 6540 (class class class)co 7405 Basecbs 17140 joincjn 18260 meetcmee 18261 Latclat 18380 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 |
| This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7361 df-ov 7408 df-oprab 7409 df-lub 18295 df-glb 18296 df-join 18297 df-meet 18298 df-lat 18381 |
| This theorem is referenced by: latleeqj1 18400 latjlej1 18402 latjlej12 18404 latnlej2 18408 latjidm 18411 latnle 18422 latabs2 18425 latledi 18426 latmlej11 18427 latjass 18432 latj13 18435 latj31 18436 latj4 18438 mod1ile 18442 mod2ile 18443 latdisdlem 18445 lubun 18464 oldmm1 38075 olj01 38083 latmassOLD 38087 omllaw5N 38105 cmtcomlemN 38106 cmtbr2N 38111 cmtbr3N 38112 cmtbr4N 38113 lecmtN 38114 omlfh1N 38116 omlfh3N 38117 omlmod1i2N 38118 cvlexchb1 38188 cvlcvr1 38197 hlatjcl 38225 exatleN 38263 cvrval3 38272 cvrexchlem 38278 cvrexch 38279 cvratlem 38280 cvrat 38281 lnnat 38286 cvrat2 38288 atcvrj2b 38291 atltcvr 38294 atlelt 38297 2atlt 38298 atexchcvrN 38299 cvrat3 38301 cvrat4 38302 2atjm 38304 4noncolr3 38312 athgt 38315 3dim0 38316 3dimlem4a 38322 1cvratex 38332 1cvrjat 38334 1cvrat 38335 ps-2 38337 3atlem1 38342 3atlem2 38343 3at 38349 2atm 38386 lplni2 38396 lplnle 38399 2llnmj 38419 2atmat 38420 lplnexllnN 38423 2llnjaN 38425 lvoli3 38436 islvol5 38438 lvoli2 38440 lvolnle3at 38441 3atnelvolN 38445 islvol2aN 38451 4atlem3 38455 4atlem4d 38461 4atlem9 38462 4atlem10a 38463 4atlem10 38465 4atlem11a 38466 4atlem11b 38467 4atlem11 38468 4atlem12a 38469 4atlem12b 38470 4atlem12 38471 4at 38472 lplncvrlvol2 38474 2lplnja 38478 2lplnmj 38481 dalem5 38526 dalem8 38529 dalem-cly 38530 dalem38 38569 dalem39 38570 dalem44 38575 dalem54 38585 linepsubN 38611 pmapsub 38627 isline2 38633 linepmap 38634 isline3 38635 lncvrelatN 38640 2llnma1b 38645 cdlema1N 38650 cdlemblem 38652 cdlemb 38653 paddasslem5 38683 paddasslem12 38690 paddasslem13 38691 pmapjoin 38711 pmapjat1 38712 pmapjlln1 38714 hlmod1i 38715 llnmod1i2 38719 atmod2i1 38720 atmod2i2 38721 llnmod2i2 38722 atmod3i1 38723 atmod3i2 38724 dalawlem2 38731 dalawlem3 38732 dalawlem5 38734 dalawlem6 38735 dalawlem7 38736 dalawlem8 38737 dalawlem11 38740 dalawlem12 38741 pmapocjN 38789 paddatclN 38808 linepsubclN 38810 pl42lem1N 38838 pl42lem2N 38839 pl42N 38842 lhp2lt 38860 lhpj1 38881 lhpmod2i2 38897 lhpmod6i1 38898 4atexlemc 38928 lautj 38952 trlval2 39022 trlcl 39023 trljat1 39025 trljat2 39026 trlle 39043 cdlemc1 39050 cdlemc2 39051 cdlemc5 39054 cdlemd2 39058 cdlemd3 39059 cdleme0aa 39069 cdleme0b 39071 cdleme0c 39072 cdleme0cp 39073 cdleme0cq 39074 cdleme0fN 39077 cdleme1b 39085 cdleme1 39086 cdleme2 39087 cdleme3b 39088 cdleme3c 39089 cdleme4a 39098 cdleme5 39099 cdleme7e 39106 cdleme8 39109 cdleme9 39112 cdleme10 39113 cdleme11fN 39123 cdleme11g 39124 cdleme11k 39127 cdleme11 39129 cdleme15b 39134 cdleme15 39137 cdleme22gb 39153 cdleme19b 39163 cdleme20d 39171 cdleme20j 39177 cdleme20l 39181 cdleme20m 39182 cdleme22e 39203 cdleme22eALTN 39204 cdleme22f 39205 cdleme23b 39209 cdleme23c 39210 cdleme28a 39229 cdleme28b 39230 cdleme29ex 39233 cdleme30a 39237 cdlemefr29exN 39261 cdleme32e 39304 cdleme35fnpq 39308 cdleme35b 39309 cdleme35c 39310 cdleme42e 39338 cdleme42i 39342 cdleme42mgN 39347 cdlemg2fv2 39459 cdlemg7fvbwN 39466 cdlemg4c 39471 cdlemg6c 39479 cdlemg10 39500 cdlemg11b 39501 cdlemg31a 39556 cdlemg31b 39557 cdlemg35 39572 trlcolem 39585 cdlemg44a 39590 trljco 39599 tendopltp 39639 cdlemh1 39674 cdlemh2 39675 cdlemi1 39677 cdlemi 39679 cdlemk4 39693 cdlemkvcl 39701 cdlemk10 39702 cdlemk11 39708 cdlemk11u 39730 cdlemk37 39773 cdlemkid1 39781 cdlemk50 39811 cdlemk51 39812 cdlemk52 39813 dialss 39905 dia2dimlem2 39924 dia2dimlem3 39925 cdlemm10N 39977 docaclN 39983 doca2N 39985 djajN 39996 diblss 40029 cdlemn2 40054 cdlemn10 40065 dihord1 40077 dihord2pre2 40085 dihord5apre 40121 dihjatc1 40170 dihmeetlem10N 40175 dihmeetlem11N 40176 djhljjN 40261 djhj 40263 dihprrnlem1N 40283 dihprrnlem2 40284 dihjat6 40293 dihjat5N 40296 dvh4dimat 40297 |
| Copyright terms: Public domain | W3C validator |