Theorem latjcl 18376

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6502  (class class class)co 7370  Basecbs 17150  joincjn 18248  meetcmee 18249  Latclat 18368

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 5226  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692

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 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-riota 7327  df-ov 7373  df-oprab 7374  df-lub 18281  df-glb 18282  df-join 18283  df-meet 18284  df-lat 18369

This theorem is referenced by:  latleeqj1  18388  latjlej1  18390  latjlej12  18392  latnlej2  18396  latjidm  18399  latnle  18410  latabs2  18413  latledi  18414  latmlej11  18415  latjass  18420  latj13  18423  latj31  18424  latj4  18426  mod1ile  18430  mod2ile  18431  latdisdlem  18433  lubun  18452  oldmm1  39622  olj01  39630  latmassOLD  39634  omllaw5N  39652  cmtcomlemN  39653  cmtbr2N  39658  cmtbr3N  39659  cmtbr4N  39660  lecmtN  39661  omlfh1N  39663  omlfh3N  39664  omlmod1i2N  39665  cvlexchb1  39735  cvlcvr1  39744  hlatjcl  39772  exatleN  39809  cvrval3  39818  cvrexchlem  39824  cvrexch  39825  cvratlem  39826  cvrat  39827  lnnat  39832  cvrat2  39834  atcvrj2b  39837  atltcvr  39840  atlelt  39843  2atlt  39844  atexchcvrN  39845  cvrat3  39847  cvrat4  39848  2atjm  39850  4noncolr3  39858  athgt  39861  3dim0  39862  3dimlem4a  39868  1cvratex  39878  1cvrjat  39880  1cvrat  39881  ps-2  39883  3atlem1  39888  3atlem2  39889  3at  39895  2atm  39932  lplni2  39942  lplnle  39945  2llnmj  39965  2atmat  39966  lplnexllnN  39969  2llnjaN  39971  lvoli3  39982  islvol5  39984  lvoli2  39986  lvolnle3at  39987  3atnelvolN  39991  islvol2aN  39997  4atlem3  40001  4atlem4d  40007  4atlem9  40008  4atlem10a  40009  4atlem10  40011  4atlem11a  40012  4atlem11b  40013  4atlem11  40014  4atlem12a  40015  4atlem12b  40016  4atlem12  40017  4at  40018  lplncvrlvol2  40020  2lplnja  40024  2lplnmj  40027  dalem5  40072  dalem8  40075  dalem-cly  40076  dalem38  40115  dalem39  40116  dalem44  40121  dalem54  40131  linepsubN  40157  pmapsub  40173  isline2  40179  linepmap  40180  isline3  40181  lncvrelatN  40186  2llnma1b  40191  cdlema1N  40196  cdlemblem  40198  cdlemb  40199  paddasslem5  40229  paddasslem12  40236  paddasslem13  40237  pmapjoin  40257  pmapjat1  40258  pmapjlln1  40260  hlmod1i  40261  llnmod1i2  40265  atmod2i1  40266  atmod2i2  40267  llnmod2i2  40268  atmod3i1  40269  atmod3i2  40270  dalawlem2  40277  dalawlem3  40278  dalawlem5  40280  dalawlem6  40281  dalawlem7  40282  dalawlem8  40283  dalawlem11  40286  dalawlem12  40287  pmapocjN  40335  paddatclN  40354  linepsubclN  40356  pl42lem1N  40384  pl42lem2N  40385  pl42N  40388  lhp2lt  40406  lhpj1  40427  lhpmod2i2  40443  lhpmod6i1  40444  4atexlemc  40474  lautj  40498  trlval2  40568  trlcl  40569  trljat1  40571  trljat2  40572  trlle  40589  cdlemc1  40596  cdlemc2  40597  cdlemc5  40600  cdlemd2  40604  cdlemd3  40605  cdleme0aa  40615  cdleme0b  40617  cdleme0c  40618  cdleme0cp  40619  cdleme0cq  40620  cdleme0fN  40623  cdleme1b  40631  cdleme1  40632  cdleme2  40633  cdleme3b  40634  cdleme3c  40635  cdleme4a  40644  cdleme5  40645  cdleme7e  40652  cdleme8  40655  cdleme9  40658  cdleme10  40659  cdleme11fN  40669  cdleme11g  40670  cdleme11k  40673  cdleme11  40675  cdleme15b  40680  cdleme15  40683  cdleme22gb  40699  cdleme19b  40709  cdleme20d  40717  cdleme20j  40723  cdleme20l  40727  cdleme20m  40728  cdleme22e  40749  cdleme22eALTN  40750  cdleme22f  40751  cdleme23b  40755  cdleme23c  40756  cdleme28a  40775  cdleme28b  40776  cdleme29ex  40779  cdleme30a  40783  cdlemefr29exN  40807  cdleme32e  40850  cdleme35fnpq  40854  cdleme35b  40855  cdleme35c  40856  cdleme42e  40884  cdleme42i  40888  cdleme42mgN  40893  cdlemg2fv2  41005  cdlemg7fvbwN  41012  cdlemg4c  41017  cdlemg6c  41025  cdlemg10  41046  cdlemg11b  41047  cdlemg31a  41102  cdlemg31b  41103  cdlemg35  41118  trlcolem  41131  cdlemg44a  41136  trljco  41145  tendopltp  41185  cdlemh1  41220  cdlemh2  41221  cdlemi1  41223  cdlemi  41225  cdlemk4  41239  cdlemkvcl  41247  cdlemk10  41248  cdlemk11  41254  cdlemk11u  41276  cdlemk37  41319  cdlemkid1  41327  cdlemk50  41357  cdlemk51  41358  cdlemk52  41359  dialss  41451  dia2dimlem2  41470  dia2dimlem3  41471  cdlemm10N  41523  docaclN  41529  doca2N  41531  djajN  41542  diblss  41575  cdlemn2  41600  cdlemn10  41611  dihord1  41623  dihord2pre2  41631  dihord5apre  41667  dihjatc1  41716  dihmeetlem10N  41721  dihmeetlem11N  41722  djhljjN  41807  djhj  41809  dihprrnlem1N  41829  dihprrnlem2  41830  dihjat6  41839  dihjat5N  41842  dvh4dimat  41843