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 38237
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 38233 . 2 (𝐾 ∈ HL β†’ 𝐾 ∈ Lat)
2 hlatjcl.b . . 3 𝐡 = (Baseβ€˜πΎ)
3 hlatjcl.a . . 3 𝐴 = (Atomsβ€˜πΎ)
42, 3atbase 38159 . 2 (𝑋 ∈ 𝐴 β†’ 𝑋 ∈ 𝐡)
52, 3atbase 38159 . 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 38133  HLchlt 38220
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 38137  df-atl 38168  df-cvlat 38192  df-hlat 38221
This theorem is referenced by:  atcvr0eq  38297  2atjm  38316  atbtwn  38317  3dim0  38328  3dimlem3a  38331  3dimlem3OLDN  38333  3dimlem4OLDN  38336  3dim3  38340  2dim  38341  ps-1  38348  hlatexch3N  38351  hlatexch4  38352  ps-2b  38353  3atlem1  38354  3atlem2  38355  llni2  38383  llnle  38389  2at0mat0  38396  2atm  38398  islpln5  38406  lplni2  38408  lplnnle2at  38412  2atnelpln  38415  islpln2a  38419  llncvrlpln2  38428  2atmat  38432  2llnjaN  38437  islvol5  38450  lvoli2  38452  lvolnle3at  38453  3atnelvolN  38457  islvol2aN  38463  4atlem0a  38464  4atlem3  38467  4atlem3a  38468  4atlem3b  38469  4atlem4a  38470  4atlem4b  38471  4atlem4c  38472  4atlem4d  38473  4atlem9  38474  4atlem10a  38475  4atlem10  38477  4atlem11a  38478  4atlem11b  38479  4atlem11  38480  4atlem12a  38481  4atlem12b  38482  4atlem12  38483  4at  38484  4at2  38485  lplncvrlvol2  38486  2lplnja  38490  dalempjqeb  38516  dalemsjteb  38517  dalemtjueb  38518  dalemply  38525  dalem1  38530  dalemcea  38531  dalem3  38535  dalem4  38536  dalem5  38538  dalem-cly  38542  dalem17  38551  dalem21  38565  dalem24  38568  dalem25  38569  dalem27  38570  dalem38  38581  dalem39  38582  dalem43  38586  dalem44  38587  dalem45  38588  dalem55  38598  dalem56  38599  dalem57  38600  2atm2atN  38656  2llnma1b  38657  2llnma3r  38659  llnmod2i2  38734  llnexchb2lem  38739  dalawlem1  38742  dalawlem2  38743  dalawlem3  38744  dalawlem4  38745  dalawlem5  38746  dalawlem6  38747  dalawlem7  38748  dalawlem8  38749  dalawlem9  38750  dalawlem11  38752  dalawlem12  38753  dalawlem15  38756  lhp2lt  38872  lhpexle2lem  38880  lhpexle3lem  38882  lhp2at0  38903  lhp2atnle  38904  lhpat3  38917  4atexlempsb  38931  4atexlemqtb  38932  4atexlemunv  38937  4atexlemtlw  38938  4atexlemc  38940  4atexlemnclw  38941  4atexlemcnd  38943  trlval3  39058  trlval4  39059  cdlemc4  39065  cdlemc5  39066  cdlemc6  39067  cdlemd2  39070  cdleme0e  39088  cdlemeulpq  39091  cdleme01N  39092  cdleme0ex1N  39094  cdleme3g  39105  cdleme3h  39106  cdleme3  39108  cdleme4  39109  cdleme4a  39110  cdleme5  39111  cdleme7aa  39113  cdleme7c  39116  cdleme7d  39117  cdleme7e  39118  cdleme7ga  39119  cdleme7  39120  cdleme9b  39123  cdleme9  39124  cdleme10  39125  cdleme11c  39132  cdleme13  39143  cdleme15b  39146  cdleme15d  39148  cdleme15  39149  cdleme16b  39150  cdleme16e  39153  cdleme16f  39154  cdleme17b  39158  cdleme22gb  39165  cdlemedb  39168  cdlemednpq  39170  cdleme20zN  39172  cdleme19a  39174  cdleme19c  39176  cdleme20aN  39180  cdleme20c  39182  cdleme20d  39183  cdleme20e  39184  cdleme20j  39189  cdleme20l  39193  cdleme21c  39198  cdleme21ct  39200  cdleme22aa  39210  cdleme22b  39212  cdleme22cN  39213  cdleme22d  39214  cdleme22e  39215  cdleme22eALTN  39216  cdleme22f  39217  cdleme22g  39219  cdleme23a  39220  cdleme23b  39221  cdleme23c  39222  cdleme28a  39241  cdleme35a  39319  cdleme35fnpq  39320  cdleme35b  39321  cdleme35c  39322  cdleme35d  39323  cdleme35e  39324  cdleme35f  39325  cdleme42a  39342  cdleme42c  39343  cdleme42h  39353  cdleme42i  39354  cdlemeg46frv  39396  cdlemeg46vrg  39398  cdlemeg46rgv  39399  cdlemeg46req  39400  cdlemf1  39432  cdlemf2  39433  cdlemg2fv2  39471  cdlemg2m  39475  cdlemg4  39488  cdlemg8b  39499  cdlemg10bALTN  39507  cdlemg10c  39510  cdlemg10  39512  cdlemg12e  39518  cdlemg12f  39519  cdlemg12g  39520  cdlemg12  39521  cdlemg13a  39522  cdlemg17a  39532  cdlemg17dALTN  39535  cdlemg17h  39539  cdlemg17  39548  cdlemg18b  39550  cdlemg19a  39554  cdlemg19  39555  cdlemg27a  39563  cdlemg27b  39567  cdlemg31a  39568  cdlemg31b  39569  cdlemg33b0  39572  cdlemg33a  39577  trlcoabs2N  39593  trlcolem  39597  cdlemg42  39600  cdlemg46  39606  cdlemh1  39686  cdlemk3  39704  cdlemk10  39714  cdlemk12  39721  cdlemkole  39724  cdlemk14  39725  cdlemk15  39726  cdlemk1u  39730  cdlemk5u  39732  cdlemk12u  39743  cdlemk37  39785  cdlemk39  39787  cdlemkid1  39793  cdlemk51  39824  cdlemk52  39825  dia2dimlem1  39935  dia2dimlem2  39936  dia2dimlem3  39937  dia2dimlem10  39944  dia2dimlem12  39946  cdlemm10N  39989  cdlemn2  40066  cdlemn10  40077  dib2dim  40114  dih2dimb  40115  dih2dimbALTN  40116  dihjatcclem1  40289  dihjatcclem2  40290  dihjatcclem4  40292  dvh4dimat  40309
  Copyright terms: Public domain W3C validator