Theorem latjcl 17478

Description: Closure of join operation in a lattice. (chjcom 28962 analog.) (Contributed by NM, 14-Sep-2011.)

Hypotheses

Ref	Expression
latjcl.b	⊢ 𝐵 = (Base‘𝐾)
latjcl.j	⊢ ∨ = (join‘𝐾)

Assertion

Ref	Expression
latjcl	⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)

Proof of Theorem latjcl

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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)

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