Theorem latjcl 18405

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6498  (class class class)co 7367  Basecbs 17179  joincjn 18277  meetcmee 18278  Latclat 18397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-lub 18310  df-glb 18311  df-join 18312  df-meet 18313  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  39663  olj01  39671  latmassOLD  39675  omllaw5N  39693  cmtcomlemN  39694  cmtbr2N  39699  cmtbr3N  39700  cmtbr4N  39701  lecmtN  39702  omlfh1N  39704  omlfh3N  39705  omlmod1i2N  39706  cvlexchb1  39776  cvlcvr1  39785  hlatjcl  39813  exatleN  39850  cvrval3  39859  cvrexchlem  39865  cvrexch  39866  cvratlem  39867  cvrat  39868  lnnat  39873  cvrat2  39875  atcvrj2b  39878  atltcvr  39881  atlelt  39884  2atlt  39885  atexchcvrN  39886  cvrat3  39888  cvrat4  39889  2atjm  39891  4noncolr3  39899  athgt  39902  3dim0  39903  3dimlem4a  39909  1cvratex  39919  1cvrjat  39921  1cvrat  39922  ps-2  39924  3atlem1  39929  3atlem2  39930  3at  39936  2atm  39973  lplni2  39983  lplnle  39986  2llnmj  40006  2atmat  40007  lplnexllnN  40010  2llnjaN  40012  lvoli3  40023  islvol5  40025  lvoli2  40027  lvolnle3at  40028  3atnelvolN  40032  islvol2aN  40038  4atlem3  40042  4atlem4d  40048  4atlem9  40049  4atlem10a  40050  4atlem10  40052  4atlem11a  40053  4atlem11b  40054  4atlem11  40055  4atlem12a  40056  4atlem12b  40057  4atlem12  40058  4at  40059  lplncvrlvol2  40061  2lplnja  40065  2lplnmj  40068  dalem5  40113  dalem8  40116  dalem-cly  40117  dalem38  40156  dalem39  40157  dalem44  40162  dalem54  40172  linepsubN  40198  pmapsub  40214  isline2  40220  linepmap  40221  isline3  40222  lncvrelatN  40227  2llnma1b  40232  cdlema1N  40237  cdlemblem  40239  cdlemb  40240  paddasslem5  40270  paddasslem12  40277  paddasslem13  40278  pmapjoin  40298  pmapjat1  40299  pmapjlln1  40301  hlmod1i  40302  llnmod1i2  40306  atmod2i1  40307  atmod2i2  40308  llnmod2i2  40309  atmod3i1  40310  atmod3i2  40311  dalawlem2  40318  dalawlem3  40319  dalawlem5  40321  dalawlem6  40322  dalawlem7  40323  dalawlem8  40324  dalawlem11  40327  dalawlem12  40328  pmapocjN  40376  paddatclN  40395  linepsubclN  40397  pl42lem1N  40425  pl42lem2N  40426  pl42N  40429  lhp2lt  40447  lhpj1  40468  lhpmod2i2  40484  lhpmod6i1  40485  4atexlemc  40515  lautj  40539  trlval2  40609  trlcl  40610  trljat1  40612  trljat2  40613  trlle  40630  cdlemc1  40637  cdlemc2  40638  cdlemc5  40641  cdlemd2  40645  cdlemd3  40646  cdleme0aa  40656  cdleme0b  40658  cdleme0c  40659  cdleme0cp  40660  cdleme0cq  40661  cdleme0fN  40664  cdleme1b  40672  cdleme1  40673  cdleme2  40674  cdleme3b  40675  cdleme3c  40676  cdleme4a  40685  cdleme5  40686  cdleme7e  40693  cdleme8  40696  cdleme9  40699  cdleme10  40700  cdleme11fN  40710  cdleme11g  40711  cdleme11k  40714  cdleme11  40716  cdleme15b  40721  cdleme15  40724  cdleme22gb  40740  cdleme19b  40750  cdleme20d  40758  cdleme20j  40764  cdleme20l  40768  cdleme20m  40769  cdleme22e  40790  cdleme22eALTN  40791  cdleme22f  40792  cdleme23b  40796  cdleme23c  40797  cdleme28a  40816  cdleme28b  40817  cdleme29ex  40820  cdleme30a  40824  cdlemefr29exN  40848  cdleme32e  40891  cdleme35fnpq  40895  cdleme35b  40896  cdleme35c  40897  cdleme42e  40925  cdleme42i  40929  cdleme42mgN  40934  cdlemg2fv2  41046  cdlemg7fvbwN  41053  cdlemg4c  41058  cdlemg6c  41066  cdlemg10  41087  cdlemg11b  41088  cdlemg31a  41143  cdlemg31b  41144  cdlemg35  41159  trlcolem  41172  cdlemg44a  41177  trljco  41186  tendopltp  41226  cdlemh1  41261  cdlemh2  41262  cdlemi1  41264  cdlemi  41266  cdlemk4  41280  cdlemkvcl  41288  cdlemk10  41289  cdlemk11  41295  cdlemk11u  41317  cdlemk37  41360  cdlemkid1  41368  cdlemk50  41398  cdlemk51  41399  cdlemk52  41400  dialss  41492  dia2dimlem2  41511  dia2dimlem3  41512  cdlemm10N  41564  docaclN  41570  doca2N  41572  djajN  41583  diblss  41616  cdlemn2  41641  cdlemn10  41652  dihord1  41664  dihord2pre2  41672  dihord5apre  41708  dihjatc1  41757  dihmeetlem10N  41762  dihmeetlem11N  41763  djhljjN  41848  djhj  41850  dihprrnlem1N  41870  dihprrnlem2  41871  dihjat6  41880  dihjat5N  41883  dvh4dimat  41884