Theorem latjcl 18628

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1569   ∈ wcel 2146  ‘cfv 6547  (class class class)co 7430  Basecbs 17402  joincjn 18500  meetcmee 18501  Latclat 18620

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7761

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6501  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-riota 7387  df-ov 7433  df-oprab 7434  df-lub 18533  df-glb 18534  df-join 18535  df-meet 18536  df-lat 18621

This theorem is used by:  latleeqj1  18640  latjlej1  18642  latjlej12  18644  latnlej2  18648  latjidm  18651  latnle  18662  latabs2  18665  latledi  18666  latmlej11  18667  latjass  18672  latj13  18675  latj31  18676  latj4  18678  mod1ile  18682  mod2ile  18683  latdisdlem  18685  lubun  18704  oldmm1  40420  olj01  40428  latmassOLD  40432  omllaw5N  40450  cmtcomlemN  40451  cmtbr2N  40456  cmtbr3N  40457  cmtbr4N  40458  lecmtN  40459  omlfh1N  40461  omlfh3N  40462  omlmod1i2N  40463  cvlexchb1  40533  cvlcvr1  40542  hlatjcl  40570  exatleN  40607  cvrval3  40616  cvrexchlem  40622  cvrexch  40623  cvratlem  40624  cvrat  40625  lnnat  40630  cvrat2  40632  atcvrj2b  40635  atltcvr  40638  atlelt  40641  2atlt  40642  atexchcvrN  40643  cvrat3  40645  cvrat4  40646  2atjm  40648  4noncolr3  40656  athgt  40659  3dim0  40660  3dimlem4a  40666  1cvratex  40676  1cvrjat  40678  1cvrat  40679  ps-2  40681  3atlem1  40686  3atlem2  40687  3at  40693  2atm  40730  lplni2  40740  lplnle  40743  2llnmj  40763  2atmat  40764  lplnexllnN  40767  2llnjaN  40769  lvoli3  40780  islvol5  40782  lvoli2  40784  lvolnle3at  40785  3atnelvolN  40789  islvol2aN  40795  4atlem3  40799  4atlem4d  40805  4atlem9  40806  4atlem10a  40807  4atlem10  40809  4atlem11a  40810  4atlem11b  40811  4atlem11  40812  4atlem12a  40813  4atlem12b  40814  4atlem12  40815  4at  40816  lplncvrlvol2  40818  2lplnja  40822  2lplnmj  40825  dalem5  40870  dalem8  40873  dalem-cly  40874  dalem38  40913  dalem39  40914  dalem44  40919  dalem54  40929  linepsubN  40955  pmapsub  40971  isline2  40977  linepmap  40978  isline3  40979  lncvrelatN  40984  2llnma1b  40989  cdlema1N  40994  cdlemblem  40996  cdlemb  40997  paddasslem5  41027  paddasslem12  41034  paddasslem13  41035  pmapjoin  41055  pmapjat1  41056  pmapjlln1  41058  hlmod1i  41059  llnmod1i2  41063  atmod2i1  41064  atmod2i2  41065  llnmod2i2  41066  atmod3i1  41067  atmod3i2  41068  dalawlem2  41075  dalawlem3  41076  dalawlem5  41078  dalawlem6  41079  dalawlem7  41080  dalawlem8  41081  dalawlem11  41084  dalawlem12  41085  pmapocjN  41133  paddatclN  41152  linepsubclN  41154  pl42lem1N  41182  pl42lem2N  41183  pl42N  41186  lhp2lt  41204  lhpj1  41225  lhpmod2i2  41241  lhpmod6i1  41242  4atexlemc  41272  lautj  41296  trlval2  41366  trlcl  41367  trljat1  41369  trljat2  41370  trlle  41387  cdlemc1  41394  cdlemc2  41395  cdlemc5  41398  cdlemd2  41402  cdlemd3  41403  cdleme0aa  41413  cdleme0b  41415  cdleme0c  41416  cdleme0cp  41417  cdleme0cq  41418  cdleme0fN  41421  cdleme1b  41429  cdleme1  41430  cdleme2  41431  cdleme3b  41432  cdleme3c  41433  cdleme4a  41442  cdleme5  41443  cdleme7e  41450  cdleme8  41453  cdleme9  41456  cdleme10  41457  cdleme11fN  41467  cdleme11g  41468  cdleme11k  41471  cdleme11  41473  cdleme15b  41478  cdleme15  41481  cdleme22gb  41497  cdleme19b  41507  cdleme20d  41515  cdleme20j  41521  cdleme20l  41525  cdleme20m  41526  cdleme22e  41547  cdleme22eALTN  41548  cdleme22f  41549  cdleme23b  41553  cdleme23c  41554  cdleme28a  41573  cdleme28b  41574  cdleme29ex  41577  cdleme30a  41581  cdlemefr29exN  41605  cdleme32e  41648  cdleme35fnpq  41652  cdleme35b  41653  cdleme35c  41654  cdleme42e  41682  cdleme42i  41686  cdleme42mgN  41691  cdlemg2fv2  41803  cdlemg7fvbwN  41810  cdlemg4c  41815  cdlemg6c  41823  cdlemg10  41844  cdlemg11b  41845  cdlemg31a  41900  cdlemg31b  41901  cdlemg35  41916  trlcolem  41929  cdlemg44a  41934  trljco  41943  tendopltp  41983  cdlemh1  42018  cdlemh2  42019  cdlemi1  42021  cdlemi  42023  cdlemk4  42037  cdlemkvcl  42045  cdlemk10  42046  cdlemk11  42052  cdlemk11u  42074  cdlemk37  42117  cdlemkid1  42125  cdlemk50  42155  cdlemk51  42156  cdlemk52  42157  dialss  42249  dia2dimlem2  42268  dia2dimlem3  42269  cdlemm10N  42321  docaclN  42327  doca2N  42329  djajN  42340  diblss  42373  cdlemn2  42398  cdlemn10  42409  dihord1  42421  dihord2pre2  42429  dihord5apre  42465  dihjatc1  42514  dihmeetlem10N  42519  dihmeetlem11N  42520  djhljjN  42605  djhj  42607  dihprrnlem1N  42627  dihprrnlem2  42628  dihjat6  42637  dihjat5N  42640  dvh4dimat  42641