Theorem latjcl 18613

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ‘cfv 6538  (class class class)co 7420  Basecbs 17387  joincjn 18485  meetcmee 18486  Latclat 18605

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-lub 18518  df-glb 18519  df-join 18520  df-meet 18521  df-lat 18606

This theorem is used by:  latleeqj1  18625  latjlej1  18627  latjlej12  18629  latnlej2  18633  latjidm  18636  latnle  18647  latabs2  18650  latledi  18651  latmlej11  18652  latjass  18657  latj13  18660  latj31  18661  latj4  18663  mod1ile  18667  mod2ile  18668  latdisdlem  18670  lubun  18689  oldmm1  40274  olj01  40282  latmassOLD  40286  omllaw5N  40304  cmtcomlemN  40305  cmtbr2N  40310  cmtbr3N  40311  cmtbr4N  40312  lecmtN  40313  omlfh1N  40315  omlfh3N  40316  omlmod1i2N  40317  cvlexchb1  40387  cvlcvr1  40396  hlatjcl  40424  exatleN  40461  cvrval3  40470  cvrexchlem  40476  cvrexch  40477  cvratlem  40478  cvrat  40479  lnnat  40484  cvrat2  40486  atcvrj2b  40489  atltcvr  40492  atlelt  40495  2atlt  40496  atexchcvrN  40497  cvrat3  40499  cvrat4  40500  2atjm  40502  4noncolr3  40510  athgt  40513  3dim0  40514  3dimlem4a  40520  1cvratex  40530  1cvrjat  40532  1cvrat  40533  ps-2  40535  3atlem1  40540  3atlem2  40541  3at  40547  2atm  40584  lplni2  40594  lplnle  40597  2llnmj  40617  2atmat  40618  lplnexllnN  40621  2llnjaN  40623  lvoli3  40634  islvol5  40636  lvoli2  40638  lvolnle3at  40639  3atnelvolN  40643  islvol2aN  40649  4atlem3  40653  4atlem4d  40659  4atlem9  40660  4atlem10a  40661  4atlem10  40663  4atlem11a  40664  4atlem11b  40665  4atlem11  40666  4atlem12a  40667  4atlem12b  40668  4atlem12  40669  4at  40670  lplncvrlvol2  40672  2lplnja  40676  2lplnmj  40679  dalem5  40724  dalem8  40727  dalem-cly  40728  dalem38  40767  dalem39  40768  dalem44  40773  dalem54  40783  linepsubN  40809  pmapsub  40825  isline2  40831  linepmap  40832  isline3  40833  lncvrelatN  40838  2llnma1b  40843  cdlema1N  40848  cdlemblem  40850  cdlemb  40851  paddasslem5  40881  paddasslem12  40888  paddasslem13  40889  pmapjoin  40909  pmapjat1  40910  pmapjlln1  40912  hlmod1i  40913  llnmod1i2  40917  atmod2i1  40918  atmod2i2  40919  llnmod2i2  40920  atmod3i1  40921  atmod3i2  40922  dalawlem2  40929  dalawlem3  40930  dalawlem5  40932  dalawlem6  40933  dalawlem7  40934  dalawlem8  40935  dalawlem11  40938  dalawlem12  40939  pmapocjN  40987  paddatclN  41006  linepsubclN  41008  pl42lem1N  41036  pl42lem2N  41037  pl42N  41040  lhp2lt  41058  lhpj1  41079  lhpmod2i2  41095  lhpmod6i1  41096  4atexlemc  41126  lautj  41150  trlval2  41220  trlcl  41221  trljat1  41223  trljat2  41224  trlle  41241  cdlemc1  41248  cdlemc2  41249  cdlemc5  41252  cdlemd2  41256  cdlemd3  41257  cdleme0aa  41267  cdleme0b  41269  cdleme0c  41270  cdleme0cp  41271  cdleme0cq  41272  cdleme0fN  41275  cdleme1b  41283  cdleme1  41284  cdleme2  41285  cdleme3b  41286  cdleme3c  41287  cdleme4a  41296  cdleme5  41297  cdleme7e  41304  cdleme8  41307  cdleme9  41310  cdleme10  41311  cdleme11fN  41321  cdleme11g  41322  cdleme11k  41325  cdleme11  41327  cdleme15b  41332  cdleme15  41335  cdleme22gb  41351  cdleme19b  41361  cdleme20d  41369  cdleme20j  41375  cdleme20l  41379  cdleme20m  41380  cdleme22e  41401  cdleme22eALTN  41402  cdleme22f  41403  cdleme23b  41407  cdleme23c  41408  cdleme28a  41427  cdleme28b  41428  cdleme29ex  41431  cdleme30a  41435  cdlemefr29exN  41459  cdleme32e  41502  cdleme35fnpq  41506  cdleme35b  41507  cdleme35c  41508  cdleme42e  41536  cdleme42i  41540  cdleme42mgN  41545  cdlemg2fv2  41657  cdlemg7fvbwN  41664  cdlemg4c  41669  cdlemg6c  41677  cdlemg10  41698  cdlemg11b  41699  cdlemg31a  41754  cdlemg31b  41755  cdlemg35  41770  trlcolem  41783  cdlemg44a  41788  trljco  41797  tendopltp  41837  cdlemh1  41872  cdlemh2  41873  cdlemi1  41875  cdlemi  41877  cdlemk4  41891  cdlemkvcl  41899  cdlemk10  41900  cdlemk11  41906  cdlemk11u  41928  cdlemk37  41971  cdlemkid1  41979  cdlemk50  42009  cdlemk51  42010  cdlemk52  42011  dialss  42103  dia2dimlem2  42122  dia2dimlem3  42123  cdlemm10N  42175  docaclN  42181  doca2N  42183  djajN  42194  diblss  42227  cdlemn2  42252  cdlemn10  42263  dihord1  42275  dihord2pre2  42283  dihord5apre  42319  dihjatc1  42368  dihmeetlem10N  42373  dihmeetlem11N  42374  djhljjN  42459  djhj  42461  dihprrnlem1N  42481  dihprrnlem2  42482  dihjat6  42491  dihjat5N  42494  dvh4dimat  42495