Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hlatjcl Structured version   Visualization version   GIF version

Theorem hlatjcl 37875
Description: Closure of join operation. Frequently-used special case of latjcl 18333 for atoms. (Contributed by NM, 15-Jun-2012.)
Hypotheses
Ref Expression
hlatjcl.b 𝐡 = (Baseβ€˜πΎ)
hlatjcl.j ∨ = (joinβ€˜πΎ)
hlatjcl.a 𝐴 = (Atomsβ€˜πΎ)
Assertion
Ref Expression
hlatjcl ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ π‘Œ ∈ 𝐴) β†’ (𝑋 ∨ π‘Œ) ∈ 𝐡)

Proof of Theorem hlatjcl
StepHypRef Expression
1 hllat 37871 . 2 (𝐾 ∈ HL β†’ 𝐾 ∈ Lat)
2 hlatjcl.b . . 3 𝐡 = (Baseβ€˜πΎ)
3 hlatjcl.a . . 3 𝐴 = (Atomsβ€˜πΎ)
42, 3atbase 37797 . 2 (𝑋 ∈ 𝐴 β†’ 𝑋 ∈ 𝐡)
52, 3atbase 37797 . 2 (π‘Œ ∈ 𝐴 β†’ π‘Œ ∈ 𝐡)
6 hlatjcl.j . . 3 ∨ = (joinβ€˜πΎ)
72, 6latjcl 18333 . 2 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ (𝑋 ∨ π‘Œ) ∈ 𝐡)
81, 4, 5, 7syl3an 1161 1 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ π‘Œ ∈ 𝐴) β†’ (𝑋 ∨ π‘Œ) ∈ 𝐡)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  β€˜cfv 6497  (class class class)co 7358  Basecbs 17088  joincjn 18205  Latclat 18325  Atomscatm 37771  HLchlt 37858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  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 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-lub 18240  df-glb 18241  df-join 18242  df-meet 18243  df-lat 18326  df-ats 37775  df-atl 37806  df-cvlat 37830  df-hlat 37859
This theorem is referenced by:  atcvr0eq  37935  2atjm  37954  atbtwn  37955  3dim0  37966  3dimlem3a  37969  3dimlem3OLDN  37971  3dimlem4OLDN  37974  3dim3  37978  2dim  37979  ps-1  37986  hlatexch3N  37989  hlatexch4  37990  ps-2b  37991  3atlem1  37992  3atlem2  37993  llni2  38021  llnle  38027  2at0mat0  38034  2atm  38036  islpln5  38044  lplni2  38046  lplnnle2at  38050  2atnelpln  38053  islpln2a  38057  llncvrlpln2  38066  2atmat  38070  2llnjaN  38075  islvol5  38088  lvoli2  38090  lvolnle3at  38091  3atnelvolN  38095  islvol2aN  38101  4atlem0a  38102  4atlem3  38105  4atlem3a  38106  4atlem3b  38107  4atlem4a  38108  4atlem4b  38109  4atlem4c  38110  4atlem4d  38111  4atlem9  38112  4atlem10a  38113  4atlem10  38115  4atlem11a  38116  4atlem11b  38117  4atlem11  38118  4atlem12a  38119  4atlem12b  38120  4atlem12  38121  4at  38122  4at2  38123  lplncvrlvol2  38124  2lplnja  38128  dalempjqeb  38154  dalemsjteb  38155  dalemtjueb  38156  dalemply  38163  dalem1  38168  dalemcea  38169  dalem3  38173  dalem4  38174  dalem5  38176  dalem-cly  38180  dalem17  38189  dalem21  38203  dalem24  38206  dalem25  38207  dalem27  38208  dalem38  38219  dalem39  38220  dalem43  38224  dalem44  38225  dalem45  38226  dalem55  38236  dalem56  38237  dalem57  38238  2atm2atN  38294  2llnma1b  38295  2llnma3r  38297  llnmod2i2  38372  llnexchb2lem  38377  dalawlem1  38380  dalawlem2  38381  dalawlem3  38382  dalawlem4  38383  dalawlem5  38384  dalawlem6  38385  dalawlem7  38386  dalawlem8  38387  dalawlem9  38388  dalawlem11  38390  dalawlem12  38391  dalawlem15  38394  lhp2lt  38510  lhpexle2lem  38518  lhpexle3lem  38520  lhp2at0  38541  lhp2atnle  38542  lhpat3  38555  4atexlempsb  38569  4atexlemqtb  38570  4atexlemunv  38575  4atexlemtlw  38576  4atexlemc  38578  4atexlemnclw  38579  4atexlemcnd  38581  trlval3  38696  trlval4  38697  cdlemc4  38703  cdlemc5  38704  cdlemc6  38705  cdlemd2  38708  cdleme0e  38726  cdlemeulpq  38729  cdleme01N  38730  cdleme0ex1N  38732  cdleme3g  38743  cdleme3h  38744  cdleme3  38746  cdleme4  38747  cdleme4a  38748  cdleme5  38749  cdleme7aa  38751  cdleme7c  38754  cdleme7d  38755  cdleme7e  38756  cdleme7ga  38757  cdleme7  38758  cdleme9b  38761  cdleme9  38762  cdleme10  38763  cdleme11c  38770  cdleme13  38781  cdleme15b  38784  cdleme15d  38786  cdleme15  38787  cdleme16b  38788  cdleme16e  38791  cdleme16f  38792  cdleme17b  38796  cdleme22gb  38803  cdlemedb  38806  cdlemednpq  38808  cdleme20zN  38810  cdleme19a  38812  cdleme19c  38814  cdleme20aN  38818  cdleme20c  38820  cdleme20d  38821  cdleme20e  38822  cdleme20j  38827  cdleme20l  38831  cdleme21c  38836  cdleme21ct  38838  cdleme22aa  38848  cdleme22b  38850  cdleme22cN  38851  cdleme22d  38852  cdleme22e  38853  cdleme22eALTN  38854  cdleme22f  38855  cdleme22g  38857  cdleme23a  38858  cdleme23b  38859  cdleme23c  38860  cdleme28a  38879  cdleme35a  38957  cdleme35fnpq  38958  cdleme35b  38959  cdleme35c  38960  cdleme35d  38961  cdleme35e  38962  cdleme35f  38963  cdleme42a  38980  cdleme42c  38981  cdleme42h  38991  cdleme42i  38992  cdlemeg46frv  39034  cdlemeg46vrg  39036  cdlemeg46rgv  39037  cdlemeg46req  39038  cdlemf1  39070  cdlemf2  39071  cdlemg2fv2  39109  cdlemg2m  39113  cdlemg4  39126  cdlemg8b  39137  cdlemg10bALTN  39145  cdlemg10c  39148  cdlemg10  39150  cdlemg12e  39156  cdlemg12f  39157  cdlemg12g  39158  cdlemg12  39159  cdlemg13a  39160  cdlemg17a  39170  cdlemg17dALTN  39173  cdlemg17h  39177  cdlemg17  39186  cdlemg18b  39188  cdlemg19a  39192  cdlemg19  39193  cdlemg27a  39201  cdlemg27b  39205  cdlemg31a  39206  cdlemg31b  39207  cdlemg33b0  39210  cdlemg33a  39215  trlcoabs2N  39231  trlcolem  39235  cdlemg42  39238  cdlemg46  39244  cdlemh1  39324  cdlemk3  39342  cdlemk10  39352  cdlemk12  39359  cdlemkole  39362  cdlemk14  39363  cdlemk15  39364  cdlemk1u  39368  cdlemk5u  39370  cdlemk12u  39381  cdlemk37  39423  cdlemk39  39425  cdlemkid1  39431  cdlemk51  39462  cdlemk52  39463  dia2dimlem1  39573  dia2dimlem2  39574  dia2dimlem3  39575  dia2dimlem10  39582  dia2dimlem12  39584  cdlemm10N  39627  cdlemn2  39704  cdlemn10  39715  dib2dim  39752  dih2dimb  39753  dih2dimbALTN  39754  dihjatcclem1  39927  dihjatcclem2  39928  dihjatcclem4  39930  dvh4dimat  39947
  Copyright terms: Public domain W3C validator