Theorem latjcl 18400

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

Syntax hints:   → wi 4   ∧ w3a 1093   = wceq 1548   ∈ wcel 2121  ‘cfv 6489  (class class class)co 7360  Basecbs 17174  joincjn 18272  meetcmee 18273  Latclat 18392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-rep 5202  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rmo 3346  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-iun 4926  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7317  df-ov 7363  df-oprab 7364  df-lub 18305  df-glb 18306  df-join 18307  df-meet 18308  df-lat 18393

This theorem is referenced by:  latleeqj1  18412  latjlej1  18414  latjlej12  18416  latnlej2  18420  latjidm  18423  latnle  18434  latabs2  18437  latledi  18438  latmlej11  18439  latjass  18444  latj13  18447  latj31  18448  latj4  18450  mod1ile  18454  mod2ile  18455  latdisdlem  18457  lubun  18476  oldmm1  39724  olj01  39732  latmassOLD  39736  omllaw5N  39754  cmtcomlemN  39755  cmtbr2N  39760  cmtbr3N  39761  cmtbr4N  39762  lecmtN  39763  omlfh1N  39765  omlfh3N  39766  omlmod1i2N  39767  cvlexchb1  39837  cvlcvr1  39846  hlatjcl  39874  exatleN  39911  cvrval3  39920  cvrexchlem  39926  cvrexch  39927  cvratlem  39928  cvrat  39929  lnnat  39934  cvrat2  39936  atcvrj2b  39939  atltcvr  39942  atlelt  39945  2atlt  39946  atexchcvrN  39947  cvrat3  39949  cvrat4  39950  2atjm  39952  4noncolr3  39960  athgt  39963  3dim0  39964  3dimlem4a  39970  1cvratex  39980  1cvrjat  39982  1cvrat  39983  ps-2  39985  3atlem1  39990  3atlem2  39991  3at  39997  2atm  40034  lplni2  40044  lplnle  40047  2llnmj  40067  2atmat  40068  lplnexllnN  40071  2llnjaN  40073  lvoli3  40084  islvol5  40086  lvoli2  40088  lvolnle3at  40089  3atnelvolN  40093  islvol2aN  40099  4atlem3  40103  4atlem4d  40109  4atlem9  40110  4atlem10a  40111  4atlem10  40113  4atlem11a  40114  4atlem11b  40115  4atlem11  40116  4atlem12a  40117  4atlem12b  40118  4atlem12  40119  4at  40120  lplncvrlvol2  40122  2lplnja  40126  2lplnmj  40129  dalem5  40174  dalem8  40177  dalem-cly  40178  dalem38  40217  dalem39  40218  dalem44  40223  dalem54  40233  linepsubN  40259  pmapsub  40275  isline2  40281  linepmap  40282  isline3  40283  lncvrelatN  40288  2llnma1b  40293  cdlema1N  40298  cdlemblem  40300  cdlemb  40301  paddasslem5  40331  paddasslem12  40338  paddasslem13  40339  pmapjoin  40359  pmapjat1  40360  pmapjlln1  40362  hlmod1i  40363  llnmod1i2  40367  atmod2i1  40368  atmod2i2  40369  llnmod2i2  40370  atmod3i1  40371  atmod3i2  40372  dalawlem2  40379  dalawlem3  40380  dalawlem5  40382  dalawlem6  40383  dalawlem7  40384  dalawlem8  40385  dalawlem11  40388  dalawlem12  40389  pmapocjN  40437  paddatclN  40456  linepsubclN  40458  pl42lem1N  40486  pl42lem2N  40487  pl42N  40490  lhp2lt  40508  lhpj1  40529  lhpmod2i2  40545  lhpmod6i1  40546  4atexlemc  40576  lautj  40600  trlval2  40670  trlcl  40671  trljat1  40673  trljat2  40674  trlle  40691  cdlemc1  40698  cdlemc2  40699  cdlemc5  40702  cdlemd2  40706  cdlemd3  40707  cdleme0aa  40717  cdleme0b  40719  cdleme0c  40720  cdleme0cp  40721  cdleme0cq  40722  cdleme0fN  40725  cdleme1b  40733  cdleme1  40734  cdleme2  40735  cdleme3b  40736  cdleme3c  40737  cdleme4a  40746  cdleme5  40747  cdleme7e  40754  cdleme8  40757  cdleme9  40760  cdleme10  40761  cdleme11fN  40771  cdleme11g  40772  cdleme11k  40775  cdleme11  40777  cdleme15b  40782  cdleme15  40785  cdleme22gb  40801  cdleme19b  40811  cdleme20d  40819  cdleme20j  40825  cdleme20l  40829  cdleme20m  40830  cdleme22e  40851  cdleme22eALTN  40852  cdleme22f  40853  cdleme23b  40857  cdleme23c  40858  cdleme28a  40877  cdleme28b  40878  cdleme29ex  40881  cdleme30a  40885  cdlemefr29exN  40909  cdleme32e  40952  cdleme35fnpq  40956  cdleme35b  40957  cdleme35c  40958  cdleme42e  40986  cdleme42i  40990  cdleme42mgN  40995  cdlemg2fv2  41107  cdlemg7fvbwN  41114  cdlemg4c  41119  cdlemg6c  41127  cdlemg10  41148  cdlemg11b  41149  cdlemg31a  41204  cdlemg31b  41205  cdlemg35  41220  trlcolem  41233  cdlemg44a  41238  trljco  41247  tendopltp  41287  cdlemh1  41322  cdlemh2  41323  cdlemi1  41325  cdlemi  41327  cdlemk4  41341  cdlemkvcl  41349  cdlemk10  41350  cdlemk11  41356  cdlemk11u  41378  cdlemk37  41421  cdlemkid1  41429  cdlemk50  41459  cdlemk51  41460  cdlemk52  41461  dialss  41553  dia2dimlem2  41572  dia2dimlem3  41573  cdlemm10N  41625  docaclN  41631  doca2N  41633  djajN  41644  diblss  41677  cdlemn2  41702  cdlemn10  41713  dihord1  41725  dihord2pre2  41733  dihord5apre  41769  dihjatc1  41818  dihmeetlem10N  41823  dihmeetlem11N  41824  djhljjN  41909  djhj  41911  dihprrnlem1N  41931  dihprrnlem2  41932  dihjat6  41941  dihjat5N  41944  dvh4dimat  41945