Theorem latjcl 18398

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6511  (class class class)co 7387  Basecbs 17179  joincjn 18272  meetcmee 18273  Latclat 18390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-lub 18305  df-glb 18306  df-join 18307  df-meet 18308  df-lat 18391

This theorem is referenced by:  latleeqj1  18410  latjlej1  18412  latjlej12  18414  latnlej2  18418  latjidm  18421  latnle  18432  latabs2  18435  latledi  18436  latmlej11  18437  latjass  18442  latj13  18445  latj31  18446  latj4  18448  mod1ile  18452  mod2ile  18453  latdisdlem  18455  lubun  18474  oldmm1  39210  olj01  39218  latmassOLD  39222  omllaw5N  39240  cmtcomlemN  39241  cmtbr2N  39246  cmtbr3N  39247  cmtbr4N  39248  lecmtN  39249  omlfh1N  39251  omlfh3N  39252  omlmod1i2N  39253  cvlexchb1  39323  cvlcvr1  39332  hlatjcl  39360  exatleN  39398  cvrval3  39407  cvrexchlem  39413  cvrexch  39414  cvratlem  39415  cvrat  39416  lnnat  39421  cvrat2  39423  atcvrj2b  39426  atltcvr  39429  atlelt  39432  2atlt  39433  atexchcvrN  39434  cvrat3  39436  cvrat4  39437  2atjm  39439  4noncolr3  39447  athgt  39450  3dim0  39451  3dimlem4a  39457  1cvratex  39467  1cvrjat  39469  1cvrat  39470  ps-2  39472  3atlem1  39477  3atlem2  39478  3at  39484  2atm  39521  lplni2  39531  lplnle  39534  2llnmj  39554  2atmat  39555  lplnexllnN  39558  2llnjaN  39560  lvoli3  39571  islvol5  39573  lvoli2  39575  lvolnle3at  39576  3atnelvolN  39580  islvol2aN  39586  4atlem3  39590  4atlem4d  39596  4atlem9  39597  4atlem10a  39598  4atlem10  39600  4atlem11a  39601  4atlem11b  39602  4atlem11  39603  4atlem12a  39604  4atlem12b  39605  4atlem12  39606  4at  39607  lplncvrlvol2  39609  2lplnja  39613  2lplnmj  39616  dalem5  39661  dalem8  39664  dalem-cly  39665  dalem38  39704  dalem39  39705  dalem44  39710  dalem54  39720  linepsubN  39746  pmapsub  39762  isline2  39768  linepmap  39769  isline3  39770  lncvrelatN  39775  2llnma1b  39780  cdlema1N  39785  cdlemblem  39787  cdlemb  39788  paddasslem5  39818  paddasslem12  39825  paddasslem13  39826  pmapjoin  39846  pmapjat1  39847  pmapjlln1  39849  hlmod1i  39850  llnmod1i2  39854  atmod2i1  39855  atmod2i2  39856  llnmod2i2  39857  atmod3i1  39858  atmod3i2  39859  dalawlem2  39866  dalawlem3  39867  dalawlem5  39869  dalawlem6  39870  dalawlem7  39871  dalawlem8  39872  dalawlem11  39875  dalawlem12  39876  pmapocjN  39924  paddatclN  39943  linepsubclN  39945  pl42lem1N  39973  pl42lem2N  39974  pl42N  39977  lhp2lt  39995  lhpj1  40016  lhpmod2i2  40032  lhpmod6i1  40033  4atexlemc  40063  lautj  40087  trlval2  40157  trlcl  40158  trljat1  40160  trljat2  40161  trlle  40178  cdlemc1  40185  cdlemc2  40186  cdlemc5  40189  cdlemd2  40193  cdlemd3  40194  cdleme0aa  40204  cdleme0b  40206  cdleme0c  40207  cdleme0cp  40208  cdleme0cq  40209  cdleme0fN  40212  cdleme1b  40220  cdleme1  40221  cdleme2  40222  cdleme3b  40223  cdleme3c  40224  cdleme4a  40233  cdleme5  40234  cdleme7e  40241  cdleme8  40244  cdleme9  40247  cdleme10  40248  cdleme11fN  40258  cdleme11g  40259  cdleme11k  40262  cdleme11  40264  cdleme15b  40269  cdleme15  40272  cdleme22gb  40288  cdleme19b  40298  cdleme20d  40306  cdleme20j  40312  cdleme20l  40316  cdleme20m  40317  cdleme22e  40338  cdleme22eALTN  40339  cdleme22f  40340  cdleme23b  40344  cdleme23c  40345  cdleme28a  40364  cdleme28b  40365  cdleme29ex  40368  cdleme30a  40372  cdlemefr29exN  40396  cdleme32e  40439  cdleme35fnpq  40443  cdleme35b  40444  cdleme35c  40445  cdleme42e  40473  cdleme42i  40477  cdleme42mgN  40482  cdlemg2fv2  40594  cdlemg7fvbwN  40601  cdlemg4c  40606  cdlemg6c  40614  cdlemg10  40635  cdlemg11b  40636  cdlemg31a  40691  cdlemg31b  40692  cdlemg35  40707  trlcolem  40720  cdlemg44a  40725  trljco  40734  tendopltp  40774  cdlemh1  40809  cdlemh2  40810  cdlemi1  40812  cdlemi  40814  cdlemk4  40828  cdlemkvcl  40836  cdlemk10  40837  cdlemk11  40843  cdlemk11u  40865  cdlemk37  40908  cdlemkid1  40916  cdlemk50  40946  cdlemk51  40947  cdlemk52  40948  dialss  41040  dia2dimlem2  41059  dia2dimlem3  41060  cdlemm10N  41112  docaclN  41118  doca2N  41120  djajN  41131  diblss  41164  cdlemn2  41189  cdlemn10  41200  dihord1  41212  dihord2pre2  41220  dihord5apre  41256  dihjatc1  41305  dihmeetlem10N  41310  dihmeetlem11N  41311  djhljjN  41396  djhj  41398  dihprrnlem1N  41418  dihprrnlem2  41419  dihjat6  41428  dihjat5N  41431  dvh4dimat  41432