Theorem latjcl 18499

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  ‘cfv 6536  (class class class)co 7410  Basecbs 17273  joincjn 18371  meetcmee 18372  Latclat 18491

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-lub 18404  df-glb 18405  df-join 18406  df-meet 18407  df-lat 18492

This theorem is used by:  latleeqj1  18511  latjlej1  18513  latjlej12  18515  latnlej2  18519  latjidm  18522  latnle  18533  latabs2  18536  latledi  18537  latmlej11  18538  latjass  18543  latj13  18546  latj31  18547  latj4  18549  mod1ile  18553  mod2ile  18554  latdisdlem  18556  lubun  18575  oldmm1  40019  olj01  40027  latmassOLD  40031  omllaw5N  40049  cmtcomlemN  40050  cmtbr2N  40055  cmtbr3N  40056  cmtbr4N  40057  lecmtN  40058  omlfh1N  40060  omlfh3N  40061  omlmod1i2N  40062  cvlexchb1  40132  cvlcvr1  40141  hlatjcl  40169  exatleN  40206  cvrval3  40215  cvrexchlem  40221  cvrexch  40222  cvratlem  40223  cvrat  40224  lnnat  40229  cvrat2  40231  atcvrj2b  40234  atltcvr  40237  atlelt  40240  2atlt  40241  atexchcvrN  40242  cvrat3  40244  cvrat4  40245  2atjm  40247  4noncolr3  40255  athgt  40258  3dim0  40259  3dimlem4a  40265  1cvratex  40275  1cvrjat  40277  1cvrat  40278  ps-2  40280  3atlem1  40285  3atlem2  40286  3at  40292  2atm  40329  lplni2  40339  lplnle  40342  2llnmj  40362  2atmat  40363  lplnexllnN  40366  2llnjaN  40368  lvoli3  40379  islvol5  40381  lvoli2  40383  lvolnle3at  40384  3atnelvolN  40388  islvol2aN  40394  4atlem3  40398  4atlem4d  40404  4atlem9  40405  4atlem10a  40406  4atlem10  40408  4atlem11a  40409  4atlem11b  40410  4atlem11  40411  4atlem12a  40412  4atlem12b  40413  4atlem12  40414  4at  40415  lplncvrlvol2  40417  2lplnja  40421  2lplnmj  40424  dalem5  40469  dalem8  40472  dalem-cly  40473  dalem38  40512  dalem39  40513  dalem44  40518  dalem54  40528  linepsubN  40554  pmapsub  40570  isline2  40576  linepmap  40577  isline3  40578  lncvrelatN  40583  2llnma1b  40588  cdlema1N  40593  cdlemblem  40595  cdlemb  40596  paddasslem5  40626  paddasslem12  40633  paddasslem13  40634  pmapjoin  40654  pmapjat1  40655  pmapjlln1  40657  hlmod1i  40658  llnmod1i2  40662  atmod2i1  40663  atmod2i2  40664  llnmod2i2  40665  atmod3i1  40666  atmod3i2  40667  dalawlem2  40674  dalawlem3  40675  dalawlem5  40677  dalawlem6  40678  dalawlem7  40679  dalawlem8  40680  dalawlem11  40683  dalawlem12  40684  pmapocjN  40732  paddatclN  40751  linepsubclN  40753  pl42lem1N  40781  pl42lem2N  40782  pl42N  40785  lhp2lt  40803  lhpj1  40824  lhpmod2i2  40840  lhpmod6i1  40841  4atexlemc  40871  lautj  40895  trlval2  40965  trlcl  40966  trljat1  40968  trljat2  40969  trlle  40986  cdlemc1  40993  cdlemc2  40994  cdlemc5  40997  cdlemd2  41001  cdlemd3  41002  cdleme0aa  41012  cdleme0b  41014  cdleme0c  41015  cdleme0cp  41016  cdleme0cq  41017  cdleme0fN  41020  cdleme1b  41028  cdleme1  41029  cdleme2  41030  cdleme3b  41031  cdleme3c  41032  cdleme4a  41041  cdleme5  41042  cdleme7e  41049  cdleme8  41052  cdleme9  41055  cdleme10  41056  cdleme11fN  41066  cdleme11g  41067  cdleme11k  41070  cdleme11  41072  cdleme15b  41077  cdleme15  41080  cdleme22gb  41096  cdleme19b  41106  cdleme20d  41114  cdleme20j  41120  cdleme20l  41124  cdleme20m  41125  cdleme22e  41146  cdleme22eALTN  41147  cdleme22f  41148  cdleme23b  41152  cdleme23c  41153  cdleme28a  41172  cdleme28b  41173  cdleme29ex  41176  cdleme30a  41180  cdlemefr29exN  41204  cdleme32e  41247  cdleme35fnpq  41251  cdleme35b  41252  cdleme35c  41253  cdleme42e  41281  cdleme42i  41285  cdleme42mgN  41290  cdlemg2fv2  41402  cdlemg7fvbwN  41409  cdlemg4c  41414  cdlemg6c  41422  cdlemg10  41443  cdlemg11b  41444  cdlemg31a  41499  cdlemg31b  41500  cdlemg35  41515  trlcolem  41528  cdlemg44a  41533  trljco  41542  tendopltp  41582  cdlemh1  41617  cdlemh2  41618  cdlemi1  41620  cdlemi  41622  cdlemk4  41636  cdlemkvcl  41644  cdlemk10  41645  cdlemk11  41651  cdlemk11u  41673  cdlemk37  41716  cdlemkid1  41724  cdlemk50  41754  cdlemk51  41755  cdlemk52  41756  dialss  41848  dia2dimlem2  41867  dia2dimlem3  41868  cdlemm10N  41920  docaclN  41926  doca2N  41928  djajN  41939  diblss  41972  cdlemn2  41997  cdlemn10  42008  dihord1  42020  dihord2pre2  42028  dihord5apre  42064  dihjatc1  42113  dihmeetlem10N  42118  dihmeetlem11N  42119  djhljjN  42204  djhj  42206  dihprrnlem1N  42226  dihprrnlem2  42227  dihjat6  42236  dihjat5N  42239  dvh4dimat  42240