Theorem latjcl 18405

Description: Closure of join operation in a lattice. (chjcom 31442 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 2730	. . 3 ⊢ (meet‘𝐾) = (meet‘𝐾)
4	1, 2, 3	latlem 18403	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∨ 𝑌) ∈ 𝐵 ∧ (𝑋(meet‘𝐾)𝑌) ∈ 𝐵))
5	4	simpld 494	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6514  (class class class)co 7390  Basecbs 17186  joincjn 18279  meetcmee 18280  Latclat 18397

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-lub 18312  df-glb 18313  df-join 18314  df-meet 18315  df-lat 18398

This theorem is referenced by:  latleeqj1  18417  latjlej1  18419  latjlej12  18421  latnlej2  18425  latjidm  18428  latnle  18439  latabs2  18442  latledi  18443  latmlej11  18444  latjass  18449  latj13  18452  latj31  18453  latj4  18455  mod1ile  18459  mod2ile  18460  latdisdlem  18462  lubun  18481  oldmm1  39217  olj01  39225  latmassOLD  39229  omllaw5N  39247  cmtcomlemN  39248  cmtbr2N  39253  cmtbr3N  39254  cmtbr4N  39255  lecmtN  39256  omlfh1N  39258  omlfh3N  39259  omlmod1i2N  39260  cvlexchb1  39330  cvlcvr1  39339  hlatjcl  39367  exatleN  39405  cvrval3  39414  cvrexchlem  39420  cvrexch  39421  cvratlem  39422  cvrat  39423  lnnat  39428  cvrat2  39430  atcvrj2b  39433  atltcvr  39436  atlelt  39439  2atlt  39440  atexchcvrN  39441  cvrat3  39443  cvrat4  39444  2atjm  39446  4noncolr3  39454  athgt  39457  3dim0  39458  3dimlem4a  39464  1cvratex  39474  1cvrjat  39476  1cvrat  39477  ps-2  39479  3atlem1  39484  3atlem2  39485  3at  39491  2atm  39528  lplni2  39538  lplnle  39541  2llnmj  39561  2atmat  39562  lplnexllnN  39565  2llnjaN  39567  lvoli3  39578  islvol5  39580  lvoli2  39582  lvolnle3at  39583  3atnelvolN  39587  islvol2aN  39593  4atlem3  39597  4atlem4d  39603  4atlem9  39604  4atlem10a  39605  4atlem10  39607  4atlem11a  39608  4atlem11b  39609  4atlem11  39610  4atlem12a  39611  4atlem12b  39612  4atlem12  39613  4at  39614  lplncvrlvol2  39616  2lplnja  39620  2lplnmj  39623  dalem5  39668  dalem8  39671  dalem-cly  39672  dalem38  39711  dalem39  39712  dalem44  39717  dalem54  39727  linepsubN  39753  pmapsub  39769  isline2  39775  linepmap  39776  isline3  39777  lncvrelatN  39782  2llnma1b  39787  cdlema1N  39792  cdlemblem  39794  cdlemb  39795  paddasslem5  39825  paddasslem12  39832  paddasslem13  39833  pmapjoin  39853  pmapjat1  39854  pmapjlln1  39856  hlmod1i  39857  llnmod1i2  39861  atmod2i1  39862  atmod2i2  39863  llnmod2i2  39864  atmod3i1  39865  atmod3i2  39866  dalawlem2  39873  dalawlem3  39874  dalawlem5  39876  dalawlem6  39877  dalawlem7  39878  dalawlem8  39879  dalawlem11  39882  dalawlem12  39883  pmapocjN  39931  paddatclN  39950  linepsubclN  39952  pl42lem1N  39980  pl42lem2N  39981  pl42N  39984  lhp2lt  40002  lhpj1  40023  lhpmod2i2  40039  lhpmod6i1  40040  4atexlemc  40070  lautj  40094  trlval2  40164  trlcl  40165  trljat1  40167  trljat2  40168  trlle  40185  cdlemc1  40192  cdlemc2  40193  cdlemc5  40196  cdlemd2  40200  cdlemd3  40201  cdleme0aa  40211  cdleme0b  40213  cdleme0c  40214  cdleme0cp  40215  cdleme0cq  40216  cdleme0fN  40219  cdleme1b  40227  cdleme1  40228  cdleme2  40229  cdleme3b  40230  cdleme3c  40231  cdleme4a  40240  cdleme5  40241  cdleme7e  40248  cdleme8  40251  cdleme9  40254  cdleme10  40255  cdleme11fN  40265  cdleme11g  40266  cdleme11k  40269  cdleme11  40271  cdleme15b  40276  cdleme15  40279  cdleme22gb  40295  cdleme19b  40305  cdleme20d  40313  cdleme20j  40319  cdleme20l  40323  cdleme20m  40324  cdleme22e  40345  cdleme22eALTN  40346  cdleme22f  40347  cdleme23b  40351  cdleme23c  40352  cdleme28a  40371  cdleme28b  40372  cdleme29ex  40375  cdleme30a  40379  cdlemefr29exN  40403  cdleme32e  40446  cdleme35fnpq  40450  cdleme35b  40451  cdleme35c  40452  cdleme42e  40480  cdleme42i  40484  cdleme42mgN  40489  cdlemg2fv2  40601  cdlemg7fvbwN  40608  cdlemg4c  40613  cdlemg6c  40621  cdlemg10  40642  cdlemg11b  40643  cdlemg31a  40698  cdlemg31b  40699  cdlemg35  40714  trlcolem  40727  cdlemg44a  40732  trljco  40741  tendopltp  40781  cdlemh1  40816  cdlemh2  40817  cdlemi1  40819  cdlemi  40821  cdlemk4  40835  cdlemkvcl  40843  cdlemk10  40844  cdlemk11  40850  cdlemk11u  40872  cdlemk37  40915  cdlemkid1  40923  cdlemk50  40953  cdlemk51  40954  cdlemk52  40955  dialss  41047  dia2dimlem2  41066  dia2dimlem3  41067  cdlemm10N  41119  docaclN  41125  doca2N  41127  djajN  41138  diblss  41171  cdlemn2  41196  cdlemn10  41207  dihord1  41219  dihord2pre2  41227  dihord5apre  41263  dihjatc1  41312  dihmeetlem10N  41317  dihmeetlem11N  41318  djhljjN  41403  djhj  41405  dihprrnlem1N  41425  dihprrnlem2  41426  dihjat6  41435  dihjat5N  41438  dvh4dimat  41439