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 29541 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 2736 | . . 3 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
4 | 1, 2, 3 | latlem 17897 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∨ 𝑌) ∈ 𝐵 ∧ (𝑋(meet‘𝐾)𝑌) ∈ 𝐵)) |
5 | 4 | simpld 498 | 1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1089 = wceq 1543 ∈ wcel 2112 ‘cfv 6358 (class class class)co 7191 Basecbs 16666 joincjn 17772 meetcmee 17773 Latclat 17891 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2708 ax-rep 5164 ax-sep 5177 ax-nul 5184 ax-pow 5243 ax-pr 5307 ax-un 7501 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2728 df-clel 2809 df-nfc 2879 df-ne 2933 df-ral 3056 df-rex 3057 df-reu 3058 df-rab 3060 df-v 3400 df-sbc 3684 df-csb 3799 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4224 df-if 4426 df-pw 4501 df-sn 4528 df-pr 4530 df-op 4534 df-uni 4806 df-iun 4892 df-br 5040 df-opab 5102 df-mpt 5121 df-id 5440 df-xp 5542 df-rel 5543 df-cnv 5544 df-co 5545 df-dm 5546 df-rn 5547 df-res 5548 df-ima 5549 df-iota 6316 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-riota 7148 df-ov 7194 df-oprab 7195 df-lub 17806 df-glb 17807 df-join 17808 df-meet 17809 df-lat 17892 |
This theorem is referenced by: latleeqj1 17911 latjlej1 17913 latjlej12 17915 latnlej2 17919 latjidm 17922 latnle 17933 latabs2 17936 latledi 17937 latmlej11 17938 latjass 17943 latj13 17946 latj31 17947 latj4 17949 mod1ile 17953 mod2ile 17954 latdisdlem 17956 lubun 17975 oldmm1 36917 olj01 36925 latmassOLD 36929 omllaw5N 36947 cmtcomlemN 36948 cmtbr2N 36953 cmtbr3N 36954 cmtbr4N 36955 lecmtN 36956 omlfh1N 36958 omlfh3N 36959 omlmod1i2N 36960 cvlexchb1 37030 cvlcvr1 37039 hlatjcl 37067 exatleN 37104 cvrval3 37113 cvrexchlem 37119 cvrexch 37120 cvratlem 37121 cvrat 37122 lnnat 37127 cvrat2 37129 atcvrj2b 37132 atltcvr 37135 atlelt 37138 2atlt 37139 atexchcvrN 37140 cvrat3 37142 cvrat4 37143 2atjm 37145 4noncolr3 37153 athgt 37156 3dim0 37157 3dimlem4a 37163 1cvratex 37173 1cvrjat 37175 1cvrat 37176 ps-2 37178 3atlem1 37183 3atlem2 37184 3at 37190 2atm 37227 lplni2 37237 lplnle 37240 2llnmj 37260 2atmat 37261 lplnexllnN 37264 2llnjaN 37266 lvoli3 37277 islvol5 37279 lvoli2 37281 lvolnle3at 37282 3atnelvolN 37286 islvol2aN 37292 4atlem3 37296 4atlem4d 37302 4atlem9 37303 4atlem10a 37304 4atlem10 37306 4atlem11a 37307 4atlem11b 37308 4atlem11 37309 4atlem12a 37310 4atlem12b 37311 4atlem12 37312 4at 37313 lplncvrlvol2 37315 2lplnja 37319 2lplnmj 37322 dalem5 37367 dalem8 37370 dalem-cly 37371 dalem38 37410 dalem39 37411 dalem44 37416 dalem54 37426 linepsubN 37452 pmapsub 37468 isline2 37474 linepmap 37475 isline3 37476 lncvrelatN 37481 2llnma1b 37486 cdlema1N 37491 cdlemblem 37493 cdlemb 37494 paddasslem5 37524 paddasslem12 37531 paddasslem13 37532 pmapjoin 37552 pmapjat1 37553 pmapjlln1 37555 hlmod1i 37556 llnmod1i2 37560 atmod2i1 37561 atmod2i2 37562 llnmod2i2 37563 atmod3i1 37564 atmod3i2 37565 dalawlem2 37572 dalawlem3 37573 dalawlem5 37575 dalawlem6 37576 dalawlem7 37577 dalawlem8 37578 dalawlem11 37581 dalawlem12 37582 pmapocjN 37630 paddatclN 37649 linepsubclN 37651 pl42lem1N 37679 pl42lem2N 37680 pl42N 37683 lhp2lt 37701 lhpj1 37722 lhpmod2i2 37738 lhpmod6i1 37739 4atexlemc 37769 lautj 37793 trlval2 37863 trlcl 37864 trljat1 37866 trljat2 37867 trlle 37884 cdlemc1 37891 cdlemc2 37892 cdlemc5 37895 cdlemd2 37899 cdlemd3 37900 cdleme0aa 37910 cdleme0b 37912 cdleme0c 37913 cdleme0cp 37914 cdleme0cq 37915 cdleme0fN 37918 cdleme1b 37926 cdleme1 37927 cdleme2 37928 cdleme3b 37929 cdleme3c 37930 cdleme4a 37939 cdleme5 37940 cdleme7e 37947 cdleme8 37950 cdleme9 37953 cdleme10 37954 cdleme11fN 37964 cdleme11g 37965 cdleme11k 37968 cdleme11 37970 cdleme15b 37975 cdleme15 37978 cdleme22gb 37994 cdleme19b 38004 cdleme20d 38012 cdleme20j 38018 cdleme20l 38022 cdleme20m 38023 cdleme22e 38044 cdleme22eALTN 38045 cdleme22f 38046 cdleme23b 38050 cdleme23c 38051 cdleme28a 38070 cdleme28b 38071 cdleme29ex 38074 cdleme30a 38078 cdlemefr29exN 38102 cdleme32e 38145 cdleme35fnpq 38149 cdleme35b 38150 cdleme35c 38151 cdleme42e 38179 cdleme42i 38183 cdleme42mgN 38188 cdlemg2fv2 38300 cdlemg7fvbwN 38307 cdlemg4c 38312 cdlemg6c 38320 cdlemg10 38341 cdlemg11b 38342 cdlemg31a 38397 cdlemg31b 38398 cdlemg35 38413 trlcolem 38426 cdlemg44a 38431 trljco 38440 tendopltp 38480 cdlemh1 38515 cdlemh2 38516 cdlemi1 38518 cdlemi 38520 cdlemk4 38534 cdlemkvcl 38542 cdlemk10 38543 cdlemk11 38549 cdlemk11u 38571 cdlemk37 38614 cdlemkid1 38622 cdlemk50 38652 cdlemk51 38653 cdlemk52 38654 dialss 38746 dia2dimlem2 38765 dia2dimlem3 38766 cdlemm10N 38818 docaclN 38824 doca2N 38826 djajN 38837 diblss 38870 cdlemn2 38895 cdlemn10 38906 dihord1 38918 dihord2pre2 38926 dihord5apre 38962 dihjatc1 39011 dihmeetlem10N 39016 dihmeetlem11N 39017 djhljjN 39102 djhj 39104 dihprrnlem1N 39124 dihprrnlem2 39125 dihjat6 39134 dihjat5N 39137 dvh4dimat 39138 |
Copyright terms: Public domain | W3C validator |