|   | 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 31525 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 2737 | . . 3 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
| 4 | 1, 2, 3 | latlem 18482 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∨ 𝑌) ∈ 𝐵 ∧ (𝑋(meet‘𝐾)𝑌) ∈ 𝐵)) | 
| 5 | 4 | simpld 494 | 1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ‘cfv 6561 (class class class)co 7431 Basecbs 17247 joincjn 18357 meetcmee 18358 Latclat 18476 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7388 df-ov 7434 df-oprab 7435 df-lub 18391 df-glb 18392 df-join 18393 df-meet 18394 df-lat 18477 | 
| This theorem is referenced by: latleeqj1 18496 latjlej1 18498 latjlej12 18500 latnlej2 18504 latjidm 18507 latnle 18518 latabs2 18521 latledi 18522 latmlej11 18523 latjass 18528 latj13 18531 latj31 18532 latj4 18534 mod1ile 18538 mod2ile 18539 latdisdlem 18541 lubun 18560 oldmm1 39218 olj01 39226 latmassOLD 39230 omllaw5N 39248 cmtcomlemN 39249 cmtbr2N 39254 cmtbr3N 39255 cmtbr4N 39256 lecmtN 39257 omlfh1N 39259 omlfh3N 39260 omlmod1i2N 39261 cvlexchb1 39331 cvlcvr1 39340 hlatjcl 39368 exatleN 39406 cvrval3 39415 cvrexchlem 39421 cvrexch 39422 cvratlem 39423 cvrat 39424 lnnat 39429 cvrat2 39431 atcvrj2b 39434 atltcvr 39437 atlelt 39440 2atlt 39441 atexchcvrN 39442 cvrat3 39444 cvrat4 39445 2atjm 39447 4noncolr3 39455 athgt 39458 3dim0 39459 3dimlem4a 39465 1cvratex 39475 1cvrjat 39477 1cvrat 39478 ps-2 39480 3atlem1 39485 3atlem2 39486 3at 39492 2atm 39529 lplni2 39539 lplnle 39542 2llnmj 39562 2atmat 39563 lplnexllnN 39566 2llnjaN 39568 lvoli3 39579 islvol5 39581 lvoli2 39583 lvolnle3at 39584 3atnelvolN 39588 islvol2aN 39594 4atlem3 39598 4atlem4d 39604 4atlem9 39605 4atlem10a 39606 4atlem10 39608 4atlem11a 39609 4atlem11b 39610 4atlem11 39611 4atlem12a 39612 4atlem12b 39613 4atlem12 39614 4at 39615 lplncvrlvol2 39617 2lplnja 39621 2lplnmj 39624 dalem5 39669 dalem8 39672 dalem-cly 39673 dalem38 39712 dalem39 39713 dalem44 39718 dalem54 39728 linepsubN 39754 pmapsub 39770 isline2 39776 linepmap 39777 isline3 39778 lncvrelatN 39783 2llnma1b 39788 cdlema1N 39793 cdlemblem 39795 cdlemb 39796 paddasslem5 39826 paddasslem12 39833 paddasslem13 39834 pmapjoin 39854 pmapjat1 39855 pmapjlln1 39857 hlmod1i 39858 llnmod1i2 39862 atmod2i1 39863 atmod2i2 39864 llnmod2i2 39865 atmod3i1 39866 atmod3i2 39867 dalawlem2 39874 dalawlem3 39875 dalawlem5 39877 dalawlem6 39878 dalawlem7 39879 dalawlem8 39880 dalawlem11 39883 dalawlem12 39884 pmapocjN 39932 paddatclN 39951 linepsubclN 39953 pl42lem1N 39981 pl42lem2N 39982 pl42N 39985 lhp2lt 40003 lhpj1 40024 lhpmod2i2 40040 lhpmod6i1 40041 4atexlemc 40071 lautj 40095 trlval2 40165 trlcl 40166 trljat1 40168 trljat2 40169 trlle 40186 cdlemc1 40193 cdlemc2 40194 cdlemc5 40197 cdlemd2 40201 cdlemd3 40202 cdleme0aa 40212 cdleme0b 40214 cdleme0c 40215 cdleme0cp 40216 cdleme0cq 40217 cdleme0fN 40220 cdleme1b 40228 cdleme1 40229 cdleme2 40230 cdleme3b 40231 cdleme3c 40232 cdleme4a 40241 cdleme5 40242 cdleme7e 40249 cdleme8 40252 cdleme9 40255 cdleme10 40256 cdleme11fN 40266 cdleme11g 40267 cdleme11k 40270 cdleme11 40272 cdleme15b 40277 cdleme15 40280 cdleme22gb 40296 cdleme19b 40306 cdleme20d 40314 cdleme20j 40320 cdleme20l 40324 cdleme20m 40325 cdleme22e 40346 cdleme22eALTN 40347 cdleme22f 40348 cdleme23b 40352 cdleme23c 40353 cdleme28a 40372 cdleme28b 40373 cdleme29ex 40376 cdleme30a 40380 cdlemefr29exN 40404 cdleme32e 40447 cdleme35fnpq 40451 cdleme35b 40452 cdleme35c 40453 cdleme42e 40481 cdleme42i 40485 cdleme42mgN 40490 cdlemg2fv2 40602 cdlemg7fvbwN 40609 cdlemg4c 40614 cdlemg6c 40622 cdlemg10 40643 cdlemg11b 40644 cdlemg31a 40699 cdlemg31b 40700 cdlemg35 40715 trlcolem 40728 cdlemg44a 40733 trljco 40742 tendopltp 40782 cdlemh1 40817 cdlemh2 40818 cdlemi1 40820 cdlemi 40822 cdlemk4 40836 cdlemkvcl 40844 cdlemk10 40845 cdlemk11 40851 cdlemk11u 40873 cdlemk37 40916 cdlemkid1 40924 cdlemk50 40954 cdlemk51 40955 cdlemk52 40956 dialss 41048 dia2dimlem2 41067 dia2dimlem3 41068 cdlemm10N 41120 docaclN 41126 doca2N 41128 djajN 41139 diblss 41172 cdlemn2 41197 cdlemn10 41208 dihord1 41220 dihord2pre2 41228 dihord5apre 41264 dihjatc1 41313 dihmeetlem10N 41318 dihmeetlem11N 41319 djhljjN 41404 djhj 41406 dihprrnlem1N 41426 dihprrnlem2 41427 dihjat6 41436 dihjat5N 41439 dvh4dimat 41440 | 
| Copyright terms: Public domain | W3C validator |