![]() |
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 31431 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 2725 | . . 3 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
4 | 1, 2, 3 | latlem 18457 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∨ 𝑌) ∈ 𝐵 ∧ (𝑋(meet‘𝐾)𝑌) ∈ 𝐵)) |
5 | 4 | simpld 493 | 1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ‘cfv 6553 (class class class)co 7423 Basecbs 17208 joincjn 18331 meetcmee 18332 Latclat 18451 |
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 2166 ax-ext 2696 ax-rep 5289 ax-sep 5303 ax-nul 5310 ax-pow 5368 ax-pr 5432 ax-un 7745 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 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 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2930 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3419 df-v 3463 df-sbc 3776 df-csb 3892 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-nul 4325 df-if 4533 df-pw 4608 df-sn 4633 df-pr 4635 df-op 4639 df-uni 4913 df-iun 5002 df-br 5153 df-opab 5215 df-mpt 5236 df-id 5579 df-xp 5687 df-rel 5688 df-cnv 5689 df-co 5690 df-dm 5691 df-rn 5692 df-res 5693 df-ima 5694 df-iota 6505 df-fun 6555 df-fn 6556 df-f 6557 df-f1 6558 df-fo 6559 df-f1o 6560 df-fv 6561 df-riota 7379 df-ov 7426 df-oprab 7427 df-lub 18366 df-glb 18367 df-join 18368 df-meet 18369 df-lat 18452 |
This theorem is referenced by: latleeqj1 18471 latjlej1 18473 latjlej12 18475 latnlej2 18479 latjidm 18482 latnle 18493 latabs2 18496 latledi 18497 latmlej11 18498 latjass 18503 latj13 18506 latj31 18507 latj4 18509 mod1ile 18513 mod2ile 18514 latdisdlem 18516 lubun 18535 oldmm1 38863 olj01 38871 latmassOLD 38875 omllaw5N 38893 cmtcomlemN 38894 cmtbr2N 38899 cmtbr3N 38900 cmtbr4N 38901 lecmtN 38902 omlfh1N 38904 omlfh3N 38905 omlmod1i2N 38906 cvlexchb1 38976 cvlcvr1 38985 hlatjcl 39013 exatleN 39051 cvrval3 39060 cvrexchlem 39066 cvrexch 39067 cvratlem 39068 cvrat 39069 lnnat 39074 cvrat2 39076 atcvrj2b 39079 atltcvr 39082 atlelt 39085 2atlt 39086 atexchcvrN 39087 cvrat3 39089 cvrat4 39090 2atjm 39092 4noncolr3 39100 athgt 39103 3dim0 39104 3dimlem4a 39110 1cvratex 39120 1cvrjat 39122 1cvrat 39123 ps-2 39125 3atlem1 39130 3atlem2 39131 3at 39137 2atm 39174 lplni2 39184 lplnle 39187 2llnmj 39207 2atmat 39208 lplnexllnN 39211 2llnjaN 39213 lvoli3 39224 islvol5 39226 lvoli2 39228 lvolnle3at 39229 3atnelvolN 39233 islvol2aN 39239 4atlem3 39243 4atlem4d 39249 4atlem9 39250 4atlem10a 39251 4atlem10 39253 4atlem11a 39254 4atlem11b 39255 4atlem11 39256 4atlem12a 39257 4atlem12b 39258 4atlem12 39259 4at 39260 lplncvrlvol2 39262 2lplnja 39266 2lplnmj 39269 dalem5 39314 dalem8 39317 dalem-cly 39318 dalem38 39357 dalem39 39358 dalem44 39363 dalem54 39373 linepsubN 39399 pmapsub 39415 isline2 39421 linepmap 39422 isline3 39423 lncvrelatN 39428 2llnma1b 39433 cdlema1N 39438 cdlemblem 39440 cdlemb 39441 paddasslem5 39471 paddasslem12 39478 paddasslem13 39479 pmapjoin 39499 pmapjat1 39500 pmapjlln1 39502 hlmod1i 39503 llnmod1i2 39507 atmod2i1 39508 atmod2i2 39509 llnmod2i2 39510 atmod3i1 39511 atmod3i2 39512 dalawlem2 39519 dalawlem3 39520 dalawlem5 39522 dalawlem6 39523 dalawlem7 39524 dalawlem8 39525 dalawlem11 39528 dalawlem12 39529 pmapocjN 39577 paddatclN 39596 linepsubclN 39598 pl42lem1N 39626 pl42lem2N 39627 pl42N 39630 lhp2lt 39648 lhpj1 39669 lhpmod2i2 39685 lhpmod6i1 39686 4atexlemc 39716 lautj 39740 trlval2 39810 trlcl 39811 trljat1 39813 trljat2 39814 trlle 39831 cdlemc1 39838 cdlemc2 39839 cdlemc5 39842 cdlemd2 39846 cdlemd3 39847 cdleme0aa 39857 cdleme0b 39859 cdleme0c 39860 cdleme0cp 39861 cdleme0cq 39862 cdleme0fN 39865 cdleme1b 39873 cdleme1 39874 cdleme2 39875 cdleme3b 39876 cdleme3c 39877 cdleme4a 39886 cdleme5 39887 cdleme7e 39894 cdleme8 39897 cdleme9 39900 cdleme10 39901 cdleme11fN 39911 cdleme11g 39912 cdleme11k 39915 cdleme11 39917 cdleme15b 39922 cdleme15 39925 cdleme22gb 39941 cdleme19b 39951 cdleme20d 39959 cdleme20j 39965 cdleme20l 39969 cdleme20m 39970 cdleme22e 39991 cdleme22eALTN 39992 cdleme22f 39993 cdleme23b 39997 cdleme23c 39998 cdleme28a 40017 cdleme28b 40018 cdleme29ex 40021 cdleme30a 40025 cdlemefr29exN 40049 cdleme32e 40092 cdleme35fnpq 40096 cdleme35b 40097 cdleme35c 40098 cdleme42e 40126 cdleme42i 40130 cdleme42mgN 40135 cdlemg2fv2 40247 cdlemg7fvbwN 40254 cdlemg4c 40259 cdlemg6c 40267 cdlemg10 40288 cdlemg11b 40289 cdlemg31a 40344 cdlemg31b 40345 cdlemg35 40360 trlcolem 40373 cdlemg44a 40378 trljco 40387 tendopltp 40427 cdlemh1 40462 cdlemh2 40463 cdlemi1 40465 cdlemi 40467 cdlemk4 40481 cdlemkvcl 40489 cdlemk10 40490 cdlemk11 40496 cdlemk11u 40518 cdlemk37 40561 cdlemkid1 40569 cdlemk50 40599 cdlemk51 40600 cdlemk52 40601 dialss 40693 dia2dimlem2 40712 dia2dimlem3 40713 cdlemm10N 40765 docaclN 40771 doca2N 40773 djajN 40784 diblss 40817 cdlemn2 40842 cdlemn10 40853 dihord1 40865 dihord2pre2 40873 dihord5apre 40909 dihjatc1 40958 dihmeetlem10N 40963 dihmeetlem11N 40964 djhljjN 41049 djhj 41051 dihprrnlem1N 41071 dihprrnlem2 41072 dihjat6 41081 dihjat5N 41084 dvh4dimat 41085 |
Copyright terms: Public domain | W3C validator |