Theorem latjcl 18495

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

Syntax hints:   → wi 4   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149  ‘cfv 6537  (class class class)co 7411  Basecbs 17269  joincjn 18367  meetcmee 18368  Latclat 18487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-lub 18400  df-glb 18401  df-join 18402  df-meet 18403  df-lat 18488

This theorem is referenced by:  latleeqj1  18507  latjlej1  18509  latjlej12  18511  latnlej2  18515  latjidm  18518  latnle  18529  latabs2  18532  latledi  18533  latmlej11  18534  latjass  18539  latj13  18542  latj31  18543  latj4  18545  mod1ile  18549  mod2ile  18550  latdisdlem  18552  lubun  18571  oldmm1  39915  olj01  39923  latmassOLD  39927  omllaw5N  39945  cmtcomlemN  39946  cmtbr2N  39951  cmtbr3N  39952  cmtbr4N  39953  lecmtN  39954  omlfh1N  39956  omlfh3N  39957  omlmod1i2N  39958  cvlexchb1  40028  cvlcvr1  40037  hlatjcl  40065  exatleN  40102  cvrval3  40111  cvrexchlem  40117  cvrexch  40118  cvratlem  40119  cvrat  40120  lnnat  40125  cvrat2  40127  atcvrj2b  40130  atltcvr  40133  atlelt  40136  2atlt  40137  atexchcvrN  40138  cvrat3  40140  cvrat4  40141  2atjm  40143  4noncolr3  40151  athgt  40154  3dim0  40155  3dimlem4a  40161  1cvratex  40171  1cvrjat  40173  1cvrat  40174  ps-2  40176  3atlem1  40181  3atlem2  40182  3at  40188  2atm  40225  lplni2  40235  lplnle  40238  2llnmj  40258  2atmat  40259  lplnexllnN  40262  2llnjaN  40264  lvoli3  40275  islvol5  40277  lvoli2  40279  lvolnle3at  40280  3atnelvolN  40284  islvol2aN  40290  4atlem3  40294  4atlem4d  40300  4atlem9  40301  4atlem10a  40302  4atlem10  40304  4atlem11a  40305  4atlem11b  40306  4atlem11  40307  4atlem12a  40308  4atlem12b  40309  4atlem12  40310  4at  40311  lplncvrlvol2  40313  2lplnja  40317  2lplnmj  40320  dalem5  40365  dalem8  40368  dalem-cly  40369  dalem38  40408  dalem39  40409  dalem44  40414  dalem54  40424  linepsubN  40450  pmapsub  40466  isline2  40472  linepmap  40473  isline3  40474  lncvrelatN  40479  2llnma1b  40484  cdlema1N  40489  cdlemblem  40491  cdlemb  40492  paddasslem5  40522  paddasslem12  40529  paddasslem13  40530  pmapjoin  40550  pmapjat1  40551  pmapjlln1  40553  hlmod1i  40554  llnmod1i2  40558  atmod2i1  40559  atmod2i2  40560  llnmod2i2  40561  atmod3i1  40562  atmod3i2  40563  dalawlem2  40570  dalawlem3  40571  dalawlem5  40573  dalawlem6  40574  dalawlem7  40575  dalawlem8  40576  dalawlem11  40579  dalawlem12  40580  pmapocjN  40628  paddatclN  40647  linepsubclN  40649  pl42lem1N  40677  pl42lem2N  40678  pl42N  40681  lhp2lt  40699  lhpj1  40720  lhpmod2i2  40736  lhpmod6i1  40737  4atexlemc  40767  lautj  40791  trlval2  40861  trlcl  40862  trljat1  40864  trljat2  40865  trlle  40882  cdlemc1  40889  cdlemc2  40890  cdlemc5  40893  cdlemd2  40897  cdlemd3  40898  cdleme0aa  40908  cdleme0b  40910  cdleme0c  40911  cdleme0cp  40912  cdleme0cq  40913  cdleme0fN  40916  cdleme1b  40924  cdleme1  40925  cdleme2  40926  cdleme3b  40927  cdleme3c  40928  cdleme4a  40937  cdleme5  40938  cdleme7e  40945  cdleme8  40948  cdleme9  40951  cdleme10  40952  cdleme11fN  40962  cdleme11g  40963  cdleme11k  40966  cdleme11  40968  cdleme15b  40973  cdleme15  40976  cdleme22gb  40992  cdleme19b  41002  cdleme20d  41010  cdleme20j  41016  cdleme20l  41020  cdleme20m  41021  cdleme22e  41042  cdleme22eALTN  41043  cdleme22f  41044  cdleme23b  41048  cdleme23c  41049  cdleme28a  41068  cdleme28b  41069  cdleme29ex  41072  cdleme30a  41076  cdlemefr29exN  41100  cdleme32e  41143  cdleme35fnpq  41147  cdleme35b  41148  cdleme35c  41149  cdleme42e  41177  cdleme42i  41181  cdleme42mgN  41186  cdlemg2fv2  41298  cdlemg7fvbwN  41305  cdlemg4c  41310  cdlemg6c  41318  cdlemg10  41339  cdlemg11b  41340  cdlemg31a  41395  cdlemg31b  41396  cdlemg35  41411  trlcolem  41424  cdlemg44a  41429  trljco  41438  tendopltp  41478  cdlemh1  41513  cdlemh2  41514  cdlemi1  41516  cdlemi  41518  cdlemk4  41532  cdlemkvcl  41540  cdlemk10  41541  cdlemk11  41547  cdlemk11u  41569  cdlemk37  41612  cdlemkid1  41620  cdlemk50  41650  cdlemk51  41651  cdlemk52  41652  dialss  41744  dia2dimlem2  41763  dia2dimlem3  41764  cdlemm10N  41816  docaclN  41822  doca2N  41824  djajN  41835  diblss  41868  cdlemn2  41893  cdlemn10  41904  dihord1  41916  dihord2pre2  41924  dihord5apre  41960  dihjatc1  42009  dihmeetlem10N  42014  dihmeetlem11N  42015  djhljjN  42100  djhj  42102  dihprrnlem1N  42122  dihprrnlem2  42123  dihjat6  42132  dihjat5N  42135  dvh4dimat  42136