Theorem latjcl 18380

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6499  (class class class)co 7369  Basecbs 17155  joincjn 18252  meetcmee 18253  Latclat 18372

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 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

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 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-lub 18285  df-glb 18286  df-join 18287  df-meet 18288  df-lat 18373

This theorem is referenced by:  latleeqj1  18392  latjlej1  18394  latjlej12  18396  latnlej2  18400  latjidm  18403  latnle  18414  latabs2  18417  latledi  18418  latmlej11  18419  latjass  18424  latj13  18427  latj31  18428  latj4  18430  mod1ile  18434  mod2ile  18435  latdisdlem  18437  lubun  18456  oldmm1  39203  olj01  39211  latmassOLD  39215  omllaw5N  39233  cmtcomlemN  39234  cmtbr2N  39239  cmtbr3N  39240  cmtbr4N  39241  lecmtN  39242  omlfh1N  39244  omlfh3N  39245  omlmod1i2N  39246  cvlexchb1  39316  cvlcvr1  39325  hlatjcl  39353  exatleN  39391  cvrval3  39400  cvrexchlem  39406  cvrexch  39407  cvratlem  39408  cvrat  39409  lnnat  39414  cvrat2  39416  atcvrj2b  39419  atltcvr  39422  atlelt  39425  2atlt  39426  atexchcvrN  39427  cvrat3  39429  cvrat4  39430  2atjm  39432  4noncolr3  39440  athgt  39443  3dim0  39444  3dimlem4a  39450  1cvratex  39460  1cvrjat  39462  1cvrat  39463  ps-2  39465  3atlem1  39470  3atlem2  39471  3at  39477  2atm  39514  lplni2  39524  lplnle  39527  2llnmj  39547  2atmat  39548  lplnexllnN  39551  2llnjaN  39553  lvoli3  39564  islvol5  39566  lvoli2  39568  lvolnle3at  39569  3atnelvolN  39573  islvol2aN  39579  4atlem3  39583  4atlem4d  39589  4atlem9  39590  4atlem10a  39591  4atlem10  39593  4atlem11a  39594  4atlem11b  39595  4atlem11  39596  4atlem12a  39597  4atlem12b  39598  4atlem12  39599  4at  39600  lplncvrlvol2  39602  2lplnja  39606  2lplnmj  39609  dalem5  39654  dalem8  39657  dalem-cly  39658  dalem38  39697  dalem39  39698  dalem44  39703  dalem54  39713  linepsubN  39739  pmapsub  39755  isline2  39761  linepmap  39762  isline3  39763  lncvrelatN  39768  2llnma1b  39773  cdlema1N  39778  cdlemblem  39780  cdlemb  39781  paddasslem5  39811  paddasslem12  39818  paddasslem13  39819  pmapjoin  39839  pmapjat1  39840  pmapjlln1  39842  hlmod1i  39843  llnmod1i2  39847  atmod2i1  39848  atmod2i2  39849  llnmod2i2  39850  atmod3i1  39851  atmod3i2  39852  dalawlem2  39859  dalawlem3  39860  dalawlem5  39862  dalawlem6  39863  dalawlem7  39864  dalawlem8  39865  dalawlem11  39868  dalawlem12  39869  pmapocjN  39917  paddatclN  39936  linepsubclN  39938  pl42lem1N  39966  pl42lem2N  39967  pl42N  39970  lhp2lt  39988  lhpj1  40009  lhpmod2i2  40025  lhpmod6i1  40026  4atexlemc  40056  lautj  40080  trlval2  40150  trlcl  40151  trljat1  40153  trljat2  40154  trlle  40171  cdlemc1  40178  cdlemc2  40179  cdlemc5  40182  cdlemd2  40186  cdlemd3  40187  cdleme0aa  40197  cdleme0b  40199  cdleme0c  40200  cdleme0cp  40201  cdleme0cq  40202  cdleme0fN  40205  cdleme1b  40213  cdleme1  40214  cdleme2  40215  cdleme3b  40216  cdleme3c  40217  cdleme4a  40226  cdleme5  40227  cdleme7e  40234  cdleme8  40237  cdleme9  40240  cdleme10  40241  cdleme11fN  40251  cdleme11g  40252  cdleme11k  40255  cdleme11  40257  cdleme15b  40262  cdleme15  40265  cdleme22gb  40281  cdleme19b  40291  cdleme20d  40299  cdleme20j  40305  cdleme20l  40309  cdleme20m  40310  cdleme22e  40331  cdleme22eALTN  40332  cdleme22f  40333  cdleme23b  40337  cdleme23c  40338  cdleme28a  40357  cdleme28b  40358  cdleme29ex  40361  cdleme30a  40365  cdlemefr29exN  40389  cdleme32e  40432  cdleme35fnpq  40436  cdleme35b  40437  cdleme35c  40438  cdleme42e  40466  cdleme42i  40470  cdleme42mgN  40475  cdlemg2fv2  40587  cdlemg7fvbwN  40594  cdlemg4c  40599  cdlemg6c  40607  cdlemg10  40628  cdlemg11b  40629  cdlemg31a  40684  cdlemg31b  40685  cdlemg35  40700  trlcolem  40713  cdlemg44a  40718  trljco  40727  tendopltp  40767  cdlemh1  40802  cdlemh2  40803  cdlemi1  40805  cdlemi  40807  cdlemk4  40821  cdlemkvcl  40829  cdlemk10  40830  cdlemk11  40836  cdlemk11u  40858  cdlemk37  40901  cdlemkid1  40909  cdlemk50  40939  cdlemk51  40940  cdlemk52  40941  dialss  41033  dia2dimlem2  41052  dia2dimlem3  41053  cdlemm10N  41105  docaclN  41111  doca2N  41113  djajN  41124  diblss  41157  cdlemn2  41182  cdlemn10  41193  dihord1  41205  dihord2pre2  41213  dihord5apre  41249  dihjatc1  41298  dihmeetlem10N  41303  dihmeetlem11N  41304  djhljjN  41389  djhj  41391  dihprrnlem1N  41411  dihprrnlem2  41412  dihjat6  41421  dihjat5N  41424  dvh4dimat  41425