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 38285
Description: Closure of join operation. Frequently-used special case of latjcl 18392 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 38281 . 2 (𝐾 ∈ HL β†’ 𝐾 ∈ Lat)
2 hlatjcl.b . . 3 𝐡 = (Baseβ€˜πΎ)
3 hlatjcl.a . . 3 𝐴 = (Atomsβ€˜πΎ)
42, 3atbase 38207 . 2 (𝑋 ∈ 𝐴 β†’ 𝑋 ∈ 𝐡)
52, 3atbase 38207 . 2 (π‘Œ ∈ 𝐴 β†’ π‘Œ ∈ 𝐡)
6 hlatjcl.j . . 3 ∨ = (joinβ€˜πΎ)
72, 6latjcl 18392 . 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 6544  (class class class)co 7409  Basecbs 17144  joincjn 18264  Latclat 18384  Atomscatm 38181  HLchlt 38268
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 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
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 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-lub 18299  df-glb 18300  df-join 18301  df-meet 18302  df-lat 18385  df-ats 38185  df-atl 38216  df-cvlat 38240  df-hlat 38269
This theorem is referenced by:  atcvr0eq  38345  2atjm  38364  atbtwn  38365  3dim0  38376  3dimlem3a  38379  3dimlem3OLDN  38381  3dimlem4OLDN  38384  3dim3  38388  2dim  38389  ps-1  38396  hlatexch3N  38399  hlatexch4  38400  ps-2b  38401  3atlem1  38402  3atlem2  38403  llni2  38431  llnle  38437  2at0mat0  38444  2atm  38446  islpln5  38454  lplni2  38456  lplnnle2at  38460  2atnelpln  38463  islpln2a  38467  llncvrlpln2  38476  2atmat  38480  2llnjaN  38485  islvol5  38498  lvoli2  38500  lvolnle3at  38501  3atnelvolN  38505  islvol2aN  38511  4atlem0a  38512  4atlem3  38515  4atlem3a  38516  4atlem3b  38517  4atlem4a  38518  4atlem4b  38519  4atlem4c  38520  4atlem4d  38521  4atlem9  38522  4atlem10a  38523  4atlem10  38525  4atlem11a  38526  4atlem11b  38527  4atlem11  38528  4atlem12a  38529  4atlem12b  38530  4atlem12  38531  4at  38532  4at2  38533  lplncvrlvol2  38534  2lplnja  38538  dalempjqeb  38564  dalemsjteb  38565  dalemtjueb  38566  dalemply  38573  dalem1  38578  dalemcea  38579  dalem3  38583  dalem4  38584  dalem5  38586  dalem-cly  38590  dalem17  38599  dalem21  38613  dalem24  38616  dalem25  38617  dalem27  38618  dalem38  38629  dalem39  38630  dalem43  38634  dalem44  38635  dalem45  38636  dalem55  38646  dalem56  38647  dalem57  38648  2atm2atN  38704  2llnma1b  38705  2llnma3r  38707  llnmod2i2  38782  llnexchb2lem  38787  dalawlem1  38790  dalawlem2  38791  dalawlem3  38792  dalawlem4  38793  dalawlem5  38794  dalawlem6  38795  dalawlem7  38796  dalawlem8  38797  dalawlem9  38798  dalawlem11  38800  dalawlem12  38801  dalawlem15  38804  lhp2lt  38920  lhpexle2lem  38928  lhpexle3lem  38930  lhp2at0  38951  lhp2atnle  38952  lhpat3  38965  4atexlempsb  38979  4atexlemqtb  38980  4atexlemunv  38985  4atexlemtlw  38986  4atexlemc  38988  4atexlemnclw  38989  4atexlemcnd  38991  trlval3  39106  trlval4  39107  cdlemc4  39113  cdlemc5  39114  cdlemc6  39115  cdlemd2  39118  cdleme0e  39136  cdlemeulpq  39139  cdleme01N  39140  cdleme0ex1N  39142  cdleme3g  39153  cdleme3h  39154  cdleme3  39156  cdleme4  39157  cdleme4a  39158  cdleme5  39159  cdleme7aa  39161  cdleme7c  39164  cdleme7d  39165  cdleme7e  39166  cdleme7ga  39167  cdleme7  39168  cdleme9b  39171  cdleme9  39172  cdleme10  39173  cdleme11c  39180  cdleme13  39191  cdleme15b  39194  cdleme15d  39196  cdleme15  39197  cdleme16b  39198  cdleme16e  39201  cdleme16f  39202  cdleme17b  39206  cdleme22gb  39213  cdlemedb  39216  cdlemednpq  39218  cdleme20zN  39220  cdleme19a  39222  cdleme19c  39224  cdleme20aN  39228  cdleme20c  39230  cdleme20d  39231  cdleme20e  39232  cdleme20j  39237  cdleme20l  39241  cdleme21c  39246  cdleme21ct  39248  cdleme22aa  39258  cdleme22b  39260  cdleme22cN  39261  cdleme22d  39262  cdleme22e  39263  cdleme22eALTN  39264  cdleme22f  39265  cdleme22g  39267  cdleme23a  39268  cdleme23b  39269  cdleme23c  39270  cdleme28a  39289  cdleme35a  39367  cdleme35fnpq  39368  cdleme35b  39369  cdleme35c  39370  cdleme35d  39371  cdleme35e  39372  cdleme35f  39373  cdleme42a  39390  cdleme42c  39391  cdleme42h  39401  cdleme42i  39402  cdlemeg46frv  39444  cdlemeg46vrg  39446  cdlemeg46rgv  39447  cdlemeg46req  39448  cdlemf1  39480  cdlemf2  39481  cdlemg2fv2  39519  cdlemg2m  39523  cdlemg4  39536  cdlemg8b  39547  cdlemg10bALTN  39555  cdlemg10c  39558  cdlemg10  39560  cdlemg12e  39566  cdlemg12f  39567  cdlemg12g  39568  cdlemg12  39569  cdlemg13a  39570  cdlemg17a  39580  cdlemg17dALTN  39583  cdlemg17h  39587  cdlemg17  39596  cdlemg18b  39598  cdlemg19a  39602  cdlemg19  39603  cdlemg27a  39611  cdlemg27b  39615  cdlemg31a  39616  cdlemg31b  39617  cdlemg33b0  39620  cdlemg33a  39625  trlcoabs2N  39641  trlcolem  39645  cdlemg42  39648  cdlemg46  39654  cdlemh1  39734  cdlemk3  39752  cdlemk10  39762  cdlemk12  39769  cdlemkole  39772  cdlemk14  39773  cdlemk15  39774  cdlemk1u  39778  cdlemk5u  39780  cdlemk12u  39791  cdlemk37  39833  cdlemk39  39835  cdlemkid1  39841  cdlemk51  39872  cdlemk52  39873  dia2dimlem1  39983  dia2dimlem2  39984  dia2dimlem3  39985  dia2dimlem10  39992  dia2dimlem12  39994  cdlemm10N  40037  cdlemn2  40114  cdlemn10  40125  dib2dim  40162  dih2dimb  40163  dih2dimbALTN  40164  dihjatcclem1  40337  dihjatcclem2  40338  dihjatcclem4  40340  dvh4dimat  40357
  Copyright terms: Public domain W3C validator