Theorem latjcl 18400

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6494  (class class class)co 7362  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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5304  ax-pr 5372  ax-un 7684

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5521  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-riota 7319  df-ov 7365  df-oprab 7366  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  39681  olj01  39689  latmassOLD  39693  omllaw5N  39711  cmtcomlemN  39712  cmtbr2N  39717  cmtbr3N  39718  cmtbr4N  39719  lecmtN  39720  omlfh1N  39722  omlfh3N  39723  omlmod1i2N  39724  cvlexchb1  39794  cvlcvr1  39803  hlatjcl  39831  exatleN  39868  cvrval3  39877  cvrexchlem  39883  cvrexch  39884  cvratlem  39885  cvrat  39886  lnnat  39891  cvrat2  39893  atcvrj2b  39896  atltcvr  39899  atlelt  39902  2atlt  39903  atexchcvrN  39904  cvrat3  39906  cvrat4  39907  2atjm  39909  4noncolr3  39917  athgt  39920  3dim0  39921  3dimlem4a  39927  1cvratex  39937  1cvrjat  39939  1cvrat  39940  ps-2  39942  3atlem1  39947  3atlem2  39948  3at  39954  2atm  39991  lplni2  40001  lplnle  40004  2llnmj  40024  2atmat  40025  lplnexllnN  40028  2llnjaN  40030  lvoli3  40041  islvol5  40043  lvoli2  40045  lvolnle3at  40046  3atnelvolN  40050  islvol2aN  40056  4atlem3  40060  4atlem4d  40066  4atlem9  40067  4atlem10a  40068  4atlem10  40070  4atlem11a  40071  4atlem11b  40072  4atlem11  40073  4atlem12a  40074  4atlem12b  40075  4atlem12  40076  4at  40077  lplncvrlvol2  40079  2lplnja  40083  2lplnmj  40086  dalem5  40131  dalem8  40134  dalem-cly  40135  dalem38  40174  dalem39  40175  dalem44  40180  dalem54  40190  linepsubN  40216  pmapsub  40232  isline2  40238  linepmap  40239  isline3  40240  lncvrelatN  40245  2llnma1b  40250  cdlema1N  40255  cdlemblem  40257  cdlemb  40258  paddasslem5  40288  paddasslem12  40295  paddasslem13  40296  pmapjoin  40316  pmapjat1  40317  pmapjlln1  40319  hlmod1i  40320  llnmod1i2  40324  atmod2i1  40325  atmod2i2  40326  llnmod2i2  40327  atmod3i1  40328  atmod3i2  40329  dalawlem2  40336  dalawlem3  40337  dalawlem5  40339  dalawlem6  40340  dalawlem7  40341  dalawlem8  40342  dalawlem11  40345  dalawlem12  40346  pmapocjN  40394  paddatclN  40413  linepsubclN  40415  pl42lem1N  40443  pl42lem2N  40444  pl42N  40447  lhp2lt  40465  lhpj1  40486  lhpmod2i2  40502  lhpmod6i1  40503  4atexlemc  40533  lautj  40557  trlval2  40627  trlcl  40628  trljat1  40630  trljat2  40631  trlle  40648  cdlemc1  40655  cdlemc2  40656  cdlemc5  40659  cdlemd2  40663  cdlemd3  40664  cdleme0aa  40674  cdleme0b  40676  cdleme0c  40677  cdleme0cp  40678  cdleme0cq  40679  cdleme0fN  40682  cdleme1b  40690  cdleme1  40691  cdleme2  40692  cdleme3b  40693  cdleme3c  40694  cdleme4a  40703  cdleme5  40704  cdleme7e  40711  cdleme8  40714  cdleme9  40717  cdleme10  40718  cdleme11fN  40728  cdleme11g  40729  cdleme11k  40732  cdleme11  40734  cdleme15b  40739  cdleme15  40742  cdleme22gb  40758  cdleme19b  40768  cdleme20d  40776  cdleme20j  40782  cdleme20l  40786  cdleme20m  40787  cdleme22e  40808  cdleme22eALTN  40809  cdleme22f  40810  cdleme23b  40814  cdleme23c  40815  cdleme28a  40834  cdleme28b  40835  cdleme29ex  40838  cdleme30a  40842  cdlemefr29exN  40866  cdleme32e  40909  cdleme35fnpq  40913  cdleme35b  40914  cdleme35c  40915  cdleme42e  40943  cdleme42i  40947  cdleme42mgN  40952  cdlemg2fv2  41064  cdlemg7fvbwN  41071  cdlemg4c  41076  cdlemg6c  41084  cdlemg10  41105  cdlemg11b  41106  cdlemg31a  41161  cdlemg31b  41162  cdlemg35  41177  trlcolem  41190  cdlemg44a  41195  trljco  41204  tendopltp  41244  cdlemh1  41279  cdlemh2  41280  cdlemi1  41282  cdlemi  41284  cdlemk4  41298  cdlemkvcl  41306  cdlemk10  41307  cdlemk11  41313  cdlemk11u  41335  cdlemk37  41378  cdlemkid1  41386  cdlemk50  41416  cdlemk51  41417  cdlemk52  41418  dialss  41510  dia2dimlem2  41529  dia2dimlem3  41530  cdlemm10N  41582  docaclN  41588  doca2N  41590  djajN  41601  diblss  41634  cdlemn2  41659  cdlemn10  41670  dihord1  41682  dihord2pre2  41690  dihord5apre  41726  dihjatc1  41775  dihmeetlem10N  41780  dihmeetlem11N  41781  djhljjN  41866  djhj  41868  dihprrnlem1N  41888  dihprrnlem2  41889  dihjat6  41898  dihjat5N  41901  dvh4dimat  41902