Theorem latjcl 18447

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108  ‘cfv 6530  (class class class)co 7403  Basecbs 17226  joincjn 18321  meetcmee 18322  Latclat 18439

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-lub 18354  df-glb 18355  df-join 18356  df-meet 18357  df-lat 18440

This theorem is referenced by:  latleeqj1  18459  latjlej1  18461  latjlej12  18463  latnlej2  18467  latjidm  18470  latnle  18481  latabs2  18484  latledi  18485  latmlej11  18486  latjass  18491  latj13  18494  latj31  18495  latj4  18497  mod1ile  18501  mod2ile  18502  latdisdlem  18504  lubun  18523  oldmm1  39181  olj01  39189  latmassOLD  39193  omllaw5N  39211  cmtcomlemN  39212  cmtbr2N  39217  cmtbr3N  39218  cmtbr4N  39219  lecmtN  39220  omlfh1N  39222  omlfh3N  39223  omlmod1i2N  39224  cvlexchb1  39294  cvlcvr1  39303  hlatjcl  39331  exatleN  39369  cvrval3  39378  cvrexchlem  39384  cvrexch  39385  cvratlem  39386  cvrat  39387  lnnat  39392  cvrat2  39394  atcvrj2b  39397  atltcvr  39400  atlelt  39403  2atlt  39404  atexchcvrN  39405  cvrat3  39407  cvrat4  39408  2atjm  39410  4noncolr3  39418  athgt  39421  3dim0  39422  3dimlem4a  39428  1cvratex  39438  1cvrjat  39440  1cvrat  39441  ps-2  39443  3atlem1  39448  3atlem2  39449  3at  39455  2atm  39492  lplni2  39502  lplnle  39505  2llnmj  39525  2atmat  39526  lplnexllnN  39529  2llnjaN  39531  lvoli3  39542  islvol5  39544  lvoli2  39546  lvolnle3at  39547  3atnelvolN  39551  islvol2aN  39557  4atlem3  39561  4atlem4d  39567  4atlem9  39568  4atlem10a  39569  4atlem10  39571  4atlem11a  39572  4atlem11b  39573  4atlem11  39574  4atlem12a  39575  4atlem12b  39576  4atlem12  39577  4at  39578  lplncvrlvol2  39580  2lplnja  39584  2lplnmj  39587  dalem5  39632  dalem8  39635  dalem-cly  39636  dalem38  39675  dalem39  39676  dalem44  39681  dalem54  39691  linepsubN  39717  pmapsub  39733  isline2  39739  linepmap  39740  isline3  39741  lncvrelatN  39746  2llnma1b  39751  cdlema1N  39756  cdlemblem  39758  cdlemb  39759  paddasslem5  39789  paddasslem12  39796  paddasslem13  39797  pmapjoin  39817  pmapjat1  39818  pmapjlln1  39820  hlmod1i  39821  llnmod1i2  39825  atmod2i1  39826  atmod2i2  39827  llnmod2i2  39828  atmod3i1  39829  atmod3i2  39830  dalawlem2  39837  dalawlem3  39838  dalawlem5  39840  dalawlem6  39841  dalawlem7  39842  dalawlem8  39843  dalawlem11  39846  dalawlem12  39847  pmapocjN  39895  paddatclN  39914  linepsubclN  39916  pl42lem1N  39944  pl42lem2N  39945  pl42N  39948  lhp2lt  39966  lhpj1  39987  lhpmod2i2  40003  lhpmod6i1  40004  4atexlemc  40034  lautj  40058  trlval2  40128  trlcl  40129  trljat1  40131  trljat2  40132  trlle  40149  cdlemc1  40156  cdlemc2  40157  cdlemc5  40160  cdlemd2  40164  cdlemd3  40165  cdleme0aa  40175  cdleme0b  40177  cdleme0c  40178  cdleme0cp  40179  cdleme0cq  40180  cdleme0fN  40183  cdleme1b  40191  cdleme1  40192  cdleme2  40193  cdleme3b  40194  cdleme3c  40195  cdleme4a  40204  cdleme5  40205  cdleme7e  40212  cdleme8  40215  cdleme9  40218  cdleme10  40219  cdleme11fN  40229  cdleme11g  40230  cdleme11k  40233  cdleme11  40235  cdleme15b  40240  cdleme15  40243  cdleme22gb  40259  cdleme19b  40269  cdleme20d  40277  cdleme20j  40283  cdleme20l  40287  cdleme20m  40288  cdleme22e  40309  cdleme22eALTN  40310  cdleme22f  40311  cdleme23b  40315  cdleme23c  40316  cdleme28a  40335  cdleme28b  40336  cdleme29ex  40339  cdleme30a  40343  cdlemefr29exN  40367  cdleme32e  40410  cdleme35fnpq  40414  cdleme35b  40415  cdleme35c  40416  cdleme42e  40444  cdleme42i  40448  cdleme42mgN  40453  cdlemg2fv2  40565  cdlemg7fvbwN  40572  cdlemg4c  40577  cdlemg6c  40585  cdlemg10  40606  cdlemg11b  40607  cdlemg31a  40662  cdlemg31b  40663  cdlemg35  40678  trlcolem  40691  cdlemg44a  40696  trljco  40705  tendopltp  40745  cdlemh1  40780  cdlemh2  40781  cdlemi1  40783  cdlemi  40785  cdlemk4  40799  cdlemkvcl  40807  cdlemk10  40808  cdlemk11  40814  cdlemk11u  40836  cdlemk37  40879  cdlemkid1  40887  cdlemk50  40917  cdlemk51  40918  cdlemk52  40919  dialss  41011  dia2dimlem2  41030  dia2dimlem3  41031  cdlemm10N  41083  docaclN  41089  doca2N  41091  djajN  41102  diblss  41135  cdlemn2  41160  cdlemn10  41171  dihord1  41183  dihord2pre2  41191  dihord5apre  41227  dihjatc1  41276  dihmeetlem10N  41281  dihmeetlem11N  41282  djhljjN  41367  djhj  41369  dihprrnlem1N  41389  dihprrnlem2  41390  dihjat6  41399  dihjat5N  41402  dvh4dimat  41403