Theorem latjcl 18522

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ‘cfv 6541  (class class class)co 7420  Basecbs 17296  joincjn 18394  meetcmee 18395  Latclat 18514

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7743

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6497  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7377  df-ov 7423  df-oprab 7424  df-lub 18427  df-glb 18428  df-join 18429  df-meet 18430  df-lat 18515

This theorem is used by:  latleeqj1  18534  latjlej1  18536  latjlej12  18538  latnlej2  18542  latjidm  18545  latnle  18556  latabs2  18559  latledi  18560  latmlej11  18561  latjass  18566  latj13  18569  latj31  18570  latj4  18572  mod1ile  18576  mod2ile  18577  latdisdlem  18579  lubun  18598  oldmm1  40054  olj01  40062  latmassOLD  40066  omllaw5N  40084  cmtcomlemN  40085  cmtbr2N  40090  cmtbr3N  40091  cmtbr4N  40092  lecmtN  40093  omlfh1N  40095  omlfh3N  40096  omlmod1i2N  40097  cvlexchb1  40167  cvlcvr1  40176  hlatjcl  40204  exatleN  40241  cvrval3  40250  cvrexchlem  40256  cvrexch  40257  cvratlem  40258  cvrat  40259  lnnat  40264  cvrat2  40266  atcvrj2b  40269  atltcvr  40272  atlelt  40275  2atlt  40276  atexchcvrN  40277  cvrat3  40279  cvrat4  40280  2atjm  40282  4noncolr3  40290  athgt  40293  3dim0  40294  3dimlem4a  40300  1cvratex  40310  1cvrjat  40312  1cvrat  40313  ps-2  40315  3atlem1  40320  3atlem2  40321  3at  40327  2atm  40364  lplni2  40374  lplnle  40377  2llnmj  40397  2atmat  40398  lplnexllnN  40401  2llnjaN  40403  lvoli3  40414  islvol5  40416  lvoli2  40418  lvolnle3at  40419  3atnelvolN  40423  islvol2aN  40429  4atlem3  40433  4atlem4d  40439  4atlem9  40440  4atlem10a  40441  4atlem10  40443  4atlem11a  40444  4atlem11b  40445  4atlem11  40446  4atlem12a  40447  4atlem12b  40448  4atlem12  40449  4at  40450  lplncvrlvol2  40452  2lplnja  40456  2lplnmj  40459  dalem5  40504  dalem8  40507  dalem-cly  40508  dalem38  40547  dalem39  40548  dalem44  40553  dalem54  40563  linepsubN  40589  pmapsub  40605  isline2  40611  linepmap  40612  isline3  40613  lncvrelatN  40618  2llnma1b  40623  cdlema1N  40628  cdlemblem  40630  cdlemb  40631  paddasslem5  40661  paddasslem12  40668  paddasslem13  40669  pmapjoin  40689  pmapjat1  40690  pmapjlln1  40692  hlmod1i  40693  llnmod1i2  40697  atmod2i1  40698  atmod2i2  40699  llnmod2i2  40700  atmod3i1  40701  atmod3i2  40702  dalawlem2  40709  dalawlem3  40710  dalawlem5  40712  dalawlem6  40713  dalawlem7  40714  dalawlem8  40715  dalawlem11  40718  dalawlem12  40719  pmapocjN  40767  paddatclN  40786  linepsubclN  40788  pl42lem1N  40816  pl42lem2N  40817  pl42N  40820  lhp2lt  40838  lhpj1  40859  lhpmod2i2  40875  lhpmod6i1  40876  4atexlemc  40906  lautj  40930  trlval2  41000  trlcl  41001  trljat1  41003  trljat2  41004  trlle  41021  cdlemc1  41028  cdlemc2  41029  cdlemc5  41032  cdlemd2  41036  cdlemd3  41037  cdleme0aa  41047  cdleme0b  41049  cdleme0c  41050  cdleme0cp  41051  cdleme0cq  41052  cdleme0fN  41055  cdleme1b  41063  cdleme1  41064  cdleme2  41065  cdleme3b  41066  cdleme3c  41067  cdleme4a  41076  cdleme5  41077  cdleme7e  41084  cdleme8  41087  cdleme9  41090  cdleme10  41091  cdleme11fN  41101  cdleme11g  41102  cdleme11k  41105  cdleme11  41107  cdleme15b  41112  cdleme15  41115  cdleme22gb  41131  cdleme19b  41141  cdleme20d  41149  cdleme20j  41155  cdleme20l  41159  cdleme20m  41160  cdleme22e  41181  cdleme22eALTN  41182  cdleme22f  41183  cdleme23b  41187  cdleme23c  41188  cdleme28a  41207  cdleme28b  41208  cdleme29ex  41211  cdleme30a  41215  cdlemefr29exN  41239  cdleme32e  41282  cdleme35fnpq  41286  cdleme35b  41287  cdleme35c  41288  cdleme42e  41316  cdleme42i  41320  cdleme42mgN  41325  cdlemg2fv2  41437  cdlemg7fvbwN  41444  cdlemg4c  41449  cdlemg6c  41457  cdlemg10  41478  cdlemg11b  41479  cdlemg31a  41534  cdlemg31b  41535  cdlemg35  41550  trlcolem  41563  cdlemg44a  41568  trljco  41577  tendopltp  41617  cdlemh1  41652  cdlemh2  41653  cdlemi1  41655  cdlemi  41657  cdlemk4  41671  cdlemkvcl  41679  cdlemk10  41680  cdlemk11  41686  cdlemk11u  41708  cdlemk37  41751  cdlemkid1  41759  cdlemk50  41789  cdlemk51  41790  cdlemk52  41791  dialss  41883  dia2dimlem2  41902  dia2dimlem3  41903  cdlemm10N  41955  docaclN  41961  doca2N  41963  djajN  41974  diblss  42007  cdlemn2  42032  cdlemn10  42043  dihord1  42055  dihord2pre2  42063  dihord5apre  42099  dihjatc1  42148  dihmeetlem10N  42153  dihmeetlem11N  42154  djhljjN  42239  djhj  42241  dihprrnlem1N  42261  dihprrnlem2  42262  dihjat6  42271  dihjat5N  42274  dvh4dimat  42275