![]() |
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 28962 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 2793 | . . 3 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
4 | 1, 2, 3 | latlem 17476 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∨ 𝑌) ∈ 𝐵 ∧ (𝑋(meet‘𝐾)𝑌) ∈ 𝐵)) |
5 | 4 | simpld 495 | 1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1078 = wceq 1520 ∈ wcel 2079 ‘cfv 6217 (class class class)co 7007 Basecbs 16300 joincjn 17371 meetcmee 17372 Latclat 17472 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-13 2342 ax-ext 2767 ax-rep 5075 ax-sep 5088 ax-nul 5095 ax-pow 5150 ax-pr 5214 ax-un 7310 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1080 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-mo 2574 df-eu 2610 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ne 2983 df-ral 3108 df-rex 3109 df-reu 3110 df-rab 3112 df-v 3434 df-sbc 3702 df-csb 3807 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-nul 4207 df-if 4376 df-pw 4449 df-sn 4467 df-pr 4469 df-op 4473 df-uni 4740 df-iun 4821 df-br 4957 df-opab 5019 df-mpt 5036 df-id 5340 df-xp 5441 df-rel 5442 df-cnv 5443 df-co 5444 df-dm 5445 df-rn 5446 df-res 5447 df-ima 5448 df-iota 6181 df-fun 6219 df-fn 6220 df-f 6221 df-f1 6222 df-fo 6223 df-f1o 6224 df-fv 6225 df-riota 6968 df-ov 7010 df-oprab 7011 df-lub 17401 df-glb 17402 df-join 17403 df-meet 17404 df-lat 17473 |
This theorem is referenced by: latleeqj1 17490 latjlej1 17492 latjlej12 17494 latnlej2 17498 latjidm 17501 latnle 17512 latabs2 17515 latledi 17516 latmlej11 17517 latjass 17522 latj13 17525 latj31 17526 latj4 17528 mod1ile 17532 mod2ile 17533 lubun 17550 latdisdlem 17616 oldmm1 35834 olj01 35842 latmassOLD 35846 omllaw5N 35864 cmtcomlemN 35865 cmtbr2N 35870 cmtbr3N 35871 cmtbr4N 35872 lecmtN 35873 omlfh1N 35875 omlfh3N 35876 omlmod1i2N 35877 cvlexchb1 35947 cvlcvr1 35956 hlatjcl 35984 exatleN 36021 cvrval3 36030 cvrexchlem 36036 cvrexch 36037 cvratlem 36038 cvrat 36039 lnnat 36044 cvrat2 36046 atcvrj2b 36049 atltcvr 36052 atlelt 36055 2atlt 36056 atexchcvrN 36057 cvrat3 36059 cvrat4 36060 2atjm 36062 4noncolr3 36070 athgt 36073 3dim0 36074 3dimlem4a 36080 1cvratex 36090 1cvrjat 36092 1cvrat 36093 ps-2 36095 3atlem1 36100 3atlem2 36101 3at 36107 2atm 36144 lplni2 36154 lplnle 36157 2llnmj 36177 2atmat 36178 lplnexllnN 36181 2llnjaN 36183 lvoli3 36194 islvol5 36196 lvoli2 36198 lvolnle3at 36199 3atnelvolN 36203 islvol2aN 36209 4atlem3 36213 4atlem4d 36219 4atlem9 36220 4atlem10a 36221 4atlem10 36223 4atlem11a 36224 4atlem11b 36225 4atlem11 36226 4atlem12a 36227 4atlem12b 36228 4atlem12 36229 4at 36230 lplncvrlvol2 36232 2lplnja 36236 2lplnmj 36239 dalem5 36284 dalem8 36287 dalem-cly 36288 dalem38 36327 dalem39 36328 dalem44 36333 dalem54 36343 linepsubN 36369 pmapsub 36385 isline2 36391 linepmap 36392 isline3 36393 lncvrelatN 36398 2llnma1b 36403 cdlema1N 36408 cdlemblem 36410 cdlemb 36411 paddasslem5 36441 paddasslem12 36448 paddasslem13 36449 pmapjoin 36469 pmapjat1 36470 pmapjlln1 36472 hlmod1i 36473 llnmod1i2 36477 atmod2i1 36478 atmod2i2 36479 llnmod2i2 36480 atmod3i1 36481 atmod3i2 36482 dalawlem2 36489 dalawlem3 36490 dalawlem5 36492 dalawlem6 36493 dalawlem7 36494 dalawlem8 36495 dalawlem11 36498 dalawlem12 36499 pmapocjN 36547 paddatclN 36566 linepsubclN 36568 pl42lem1N 36596 pl42lem2N 36597 pl42N 36600 lhp2lt 36618 lhpj1 36639 lhpmod2i2 36655 lhpmod6i1 36656 4atexlemc 36686 lautj 36710 trlval2 36780 trlcl 36781 trljat1 36783 trljat2 36784 trlle 36801 cdlemc1 36808 cdlemc2 36809 cdlemc5 36812 cdlemd2 36816 cdlemd3 36817 cdleme0aa 36827 cdleme0b 36829 cdleme0c 36830 cdleme0cp 36831 cdleme0cq 36832 cdleme0fN 36835 cdleme1b 36843 cdleme1 36844 cdleme2 36845 cdleme3b 36846 cdleme3c 36847 cdleme4a 36856 cdleme5 36857 cdleme7e 36864 cdleme8 36867 cdleme9 36870 cdleme10 36871 cdleme11fN 36881 cdleme11g 36882 cdleme11k 36885 cdleme11 36887 cdleme15b 36892 cdleme15 36895 cdleme22gb 36911 cdleme19b 36921 cdleme20d 36929 cdleme20j 36935 cdleme20l 36939 cdleme20m 36940 cdleme22e 36961 cdleme22eALTN 36962 cdleme22f 36963 cdleme23b 36967 cdleme23c 36968 cdleme28a 36987 cdleme28b 36988 cdleme29ex 36991 cdleme30a 36995 cdlemefr29exN 37019 cdleme32e 37062 cdleme35fnpq 37066 cdleme35b 37067 cdleme35c 37068 cdleme42e 37096 cdleme42i 37100 cdleme42mgN 37105 cdlemg2fv2 37217 cdlemg7fvbwN 37224 cdlemg4c 37229 cdlemg6c 37237 cdlemg10 37258 cdlemg11b 37259 cdlemg31a 37314 cdlemg31b 37315 cdlemg35 37330 trlcolem 37343 cdlemg44a 37348 trljco 37357 tendopltp 37397 cdlemh1 37432 cdlemh2 37433 cdlemi1 37435 cdlemi 37437 cdlemk4 37451 cdlemkvcl 37459 cdlemk10 37460 cdlemk11 37466 cdlemk11u 37488 cdlemk37 37531 cdlemkid1 37539 cdlemk50 37569 cdlemk51 37570 cdlemk52 37571 dialss 37663 dia2dimlem2 37682 dia2dimlem3 37683 cdlemm10N 37735 docaclN 37741 doca2N 37743 djajN 37754 diblss 37787 cdlemn2 37812 cdlemn10 37823 dihord1 37835 dihord2pre2 37843 dihord5apre 37879 dihjatc1 37928 dihmeetlem10N 37933 dihmeetlem11N 37934 djhljjN 38019 djhj 38021 dihprrnlem1N 38041 dihprrnlem2 38042 dihjat6 38051 dihjat5N 38054 dvh4dimat 38055 |
Copyright terms: Public domain | W3C validator |