Theorem latjcl 18496

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105  ‘cfv 6562  (class class class)co 7430  Basecbs 17244  joincjn 18368  meetcmee 18369  Latclat 18488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-lub 18403  df-glb 18404  df-join 18405  df-meet 18406  df-lat 18489

This theorem is referenced by:  latleeqj1  18508  latjlej1  18510  latjlej12  18512  latnlej2  18516  latjidm  18519  latnle  18530  latabs2  18533  latledi  18534  latmlej11  18535  latjass  18540  latj13  18543  latj31  18544  latj4  18546  mod1ile  18550  mod2ile  18551  latdisdlem  18553  lubun  18572  oldmm1  39198  olj01  39206  latmassOLD  39210  omllaw5N  39228  cmtcomlemN  39229  cmtbr2N  39234  cmtbr3N  39235  cmtbr4N  39236  lecmtN  39237  omlfh1N  39239  omlfh3N  39240  omlmod1i2N  39241  cvlexchb1  39311  cvlcvr1  39320  hlatjcl  39348  exatleN  39386  cvrval3  39395  cvrexchlem  39401  cvrexch  39402  cvratlem  39403  cvrat  39404  lnnat  39409  cvrat2  39411  atcvrj2b  39414  atltcvr  39417  atlelt  39420  2atlt  39421  atexchcvrN  39422  cvrat3  39424  cvrat4  39425  2atjm  39427  4noncolr3  39435  athgt  39438  3dim0  39439  3dimlem4a  39445  1cvratex  39455  1cvrjat  39457  1cvrat  39458  ps-2  39460  3atlem1  39465  3atlem2  39466  3at  39472  2atm  39509  lplni2  39519  lplnle  39522  2llnmj  39542  2atmat  39543  lplnexllnN  39546  2llnjaN  39548  lvoli3  39559  islvol5  39561  lvoli2  39563  lvolnle3at  39564  3atnelvolN  39568  islvol2aN  39574  4atlem3  39578  4atlem4d  39584  4atlem9  39585  4atlem10a  39586  4atlem10  39588  4atlem11a  39589  4atlem11b  39590  4atlem11  39591  4atlem12a  39592  4atlem12b  39593  4atlem12  39594  4at  39595  lplncvrlvol2  39597  2lplnja  39601  2lplnmj  39604  dalem5  39649  dalem8  39652  dalem-cly  39653  dalem38  39692  dalem39  39693  dalem44  39698  dalem54  39708  linepsubN  39734  pmapsub  39750  isline2  39756  linepmap  39757  isline3  39758  lncvrelatN  39763  2llnma1b  39768  cdlema1N  39773  cdlemblem  39775  cdlemb  39776  paddasslem5  39806  paddasslem12  39813  paddasslem13  39814  pmapjoin  39834  pmapjat1  39835  pmapjlln1  39837  hlmod1i  39838  llnmod1i2  39842  atmod2i1  39843  atmod2i2  39844  llnmod2i2  39845  atmod3i1  39846  atmod3i2  39847  dalawlem2  39854  dalawlem3  39855  dalawlem5  39857  dalawlem6  39858  dalawlem7  39859  dalawlem8  39860  dalawlem11  39863  dalawlem12  39864  pmapocjN  39912  paddatclN  39931  linepsubclN  39933  pl42lem1N  39961  pl42lem2N  39962  pl42N  39965  lhp2lt  39983  lhpj1  40004  lhpmod2i2  40020  lhpmod6i1  40021  4atexlemc  40051  lautj  40075  trlval2  40145  trlcl  40146  trljat1  40148  trljat2  40149  trlle  40166  cdlemc1  40173  cdlemc2  40174  cdlemc5  40177  cdlemd2  40181  cdlemd3  40182  cdleme0aa  40192  cdleme0b  40194  cdleme0c  40195  cdleme0cp  40196  cdleme0cq  40197  cdleme0fN  40200  cdleme1b  40208  cdleme1  40209  cdleme2  40210  cdleme3b  40211  cdleme3c  40212  cdleme4a  40221  cdleme5  40222  cdleme7e  40229  cdleme8  40232  cdleme9  40235  cdleme10  40236  cdleme11fN  40246  cdleme11g  40247  cdleme11k  40250  cdleme11  40252  cdleme15b  40257  cdleme15  40260  cdleme22gb  40276  cdleme19b  40286  cdleme20d  40294  cdleme20j  40300  cdleme20l  40304  cdleme20m  40305  cdleme22e  40326  cdleme22eALTN  40327  cdleme22f  40328  cdleme23b  40332  cdleme23c  40333  cdleme28a  40352  cdleme28b  40353  cdleme29ex  40356  cdleme30a  40360  cdlemefr29exN  40384  cdleme32e  40427  cdleme35fnpq  40431  cdleme35b  40432  cdleme35c  40433  cdleme42e  40461  cdleme42i  40465  cdleme42mgN  40470  cdlemg2fv2  40582  cdlemg7fvbwN  40589  cdlemg4c  40594  cdlemg6c  40602  cdlemg10  40623  cdlemg11b  40624  cdlemg31a  40679  cdlemg31b  40680  cdlemg35  40695  trlcolem  40708  cdlemg44a  40713  trljco  40722  tendopltp  40762  cdlemh1  40797  cdlemh2  40798  cdlemi1  40800  cdlemi  40802  cdlemk4  40816  cdlemkvcl  40824  cdlemk10  40825  cdlemk11  40831  cdlemk11u  40853  cdlemk37  40896  cdlemkid1  40904  cdlemk50  40934  cdlemk51  40935  cdlemk52  40936  dialss  41028  dia2dimlem2  41047  dia2dimlem3  41048  cdlemm10N  41100  docaclN  41106  doca2N  41108  djajN  41119  diblss  41152  cdlemn2  41177  cdlemn10  41188  dihord1  41200  dihord2pre2  41208  dihord5apre  41244  dihjatc1  41293  dihmeetlem10N  41298  dihmeetlem11N  41299  djhljjN  41384  djhj  41386  dihprrnlem1N  41406  dihprrnlem2  41407  dihjat6  41416  dihjat5N  41419  dvh4dimat  41420