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

Theorem atbase 37797
Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 31328 analog.) (Contributed by NM, 10-Oct-2011.)
Hypotheses
Ref Expression
atombase.b 𝐡 = (Baseβ€˜πΎ)
atombase.a 𝐴 = (Atomsβ€˜πΎ)
Assertion
Ref Expression
atbase (𝑃 ∈ 𝐴 β†’ 𝑃 ∈ 𝐡)

Proof of Theorem atbase
StepHypRef Expression
1 n0i 4294 . . . 4 (𝑃 ∈ 𝐴 β†’ Β¬ 𝐴 = βˆ…)
2 atombase.a . . . . 5 𝐴 = (Atomsβ€˜πΎ)
32eqeq1i 2738 . . . 4 (𝐴 = βˆ… ↔ (Atomsβ€˜πΎ) = βˆ…)
41, 3sylnib 328 . . 3 (𝑃 ∈ 𝐴 β†’ Β¬ (Atomsβ€˜πΎ) = βˆ…)
5 fvprc 6835 . . 3 (Β¬ 𝐾 ∈ V β†’ (Atomsβ€˜πΎ) = βˆ…)
64, 5nsyl2 141 . 2 (𝑃 ∈ 𝐴 β†’ 𝐾 ∈ V)
7 atombase.b . . . 4 𝐡 = (Baseβ€˜πΎ)
8 eqid 2733 . . . 4 (0.β€˜πΎ) = (0.β€˜πΎ)
9 eqid 2733 . . . 4 ( β‹– β€˜πΎ) = ( β‹– β€˜πΎ)
107, 8, 9, 2isat 37794 . . 3 (𝐾 ∈ V β†’ (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐡 ∧ (0.β€˜πΎ)( β‹– β€˜πΎ)𝑃)))
1110simprbda 500 . 2 ((𝐾 ∈ V ∧ 𝑃 ∈ 𝐴) β†’ 𝑃 ∈ 𝐡)
126, 11mpancom 687 1 (𝑃 ∈ 𝐴 β†’ 𝑃 ∈ 𝐡)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   = wceq 1542   ∈ wcel 2107  Vcvv 3444  βˆ…c0 4283   class class class wbr 5106  β€˜cfv 6497  Basecbs 17088  0.cp0 18317   β‹– ccvr 37770  Atomscatm 37771
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-sep 5257  ax-nul 5264  ax-pr 5385
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-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  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-iota 6449  df-fun 6499  df-fv 6505  df-ats 37775
This theorem is referenced by:  atssbase  37798  0ltat  37799  leatb  37800  meetat  37804  atnle0  37817  atlen0  37818  atcmp  37819  atcvreq0  37822  atncvrN  37823  atnle  37825  atnem0  37826  atlatmstc  37827  atlatle  37828  cvlexch2  37837  cvlexchb1  37838  cvlexchb2  37839  cvlatexchb1  37842  cvlatexchb2  37843  cvlatexch1  37844  cvlatexch2  37845  cvlatexch3  37846  cvlcvr1  37847  cvlcvrp  37848  cvlatcvr1  37849  cvlatcvr2  37850  cvlsupr2  37851  cvlsupr7  37856  cvlsupr8  37857  hlatjcl  37875  hlatjcom  37876  hlatjidm  37877  hlatjass  37878  hlatj32  37880  hlatj4  37882  hlatlej1  37883  atnlej1  37888  atnlej2  37889  hlrelat5N  37910  hlrelat  37911  hlrelat2  37912  exatleN  37913  cvr2N  37920  hlrelat3  37921  cvrval3  37922  cvrval5  37924  cvrexchlem  37928  cvratlem  37930  cvrat  37931  atcvr0eq  37935  lnnat  37936  cvrat2  37938  atcvrneN  37939  atcvrj1  37940  atcvrj2b  37941  atltcvr  37944  atle  37945  atlelt  37947  2atlt  37948  atexchcvrN  37949  cvrat3  37951  cvrat4  37952  cvrat42  37953  2atjm  37954  atbtwn  37955  3noncolr2  37958  4noncolr3  37962  athgt  37965  3dim0  37966  3dimlem3a  37969  3dimlem3OLDN  37971  3dimlem4a  37972  3dimlem4OLDN  37974  3dim3  37978  2dim  37979  1cvratex  37982  1cvrjat  37984  1cvrat  37985  ps-1  37986  ps-2  37987  hlatexch3N  37989  hlatexch4  37990  ps-2b  37991  3atlem1  37992  3atlem2  37993  3atlem4  37995  3atlem5  37996  3atlem6  37997  3at  37999  islln3  38019  llnnleat  38022  llnn0  38025  llnle  38027  llnexatN  38030  llncmp  38031  2llnmat  38033  2at0mat0  38034  2atm  38036  ps-2c  38037  lplni2  38046  lplnle  38049  lplnnle2at  38050  lplnn0N  38056  islpln2a  38057  2atmat  38070  lplnexllnN  38073  2llnjaN  38075  2llnm4  38079  2llnmeqat  38080  lvoli3  38086  islvol5  38088  lvoli2  38090  lvolnle3at  38091  3atnelvolN  38095  lvoln0N  38100  islvol2aN  38101  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  4at2  38123  lplncvrlvol2  38124  2lplnja  38128  dalempeb  38148  dalemqeb  38149  dalemreb  38150  dalemseb  38151  dalemteb  38152  dalemueb  38153  dalem3  38173  dalem16  38188  dalemcceb  38198  dalem21  38203  dalem25  38207  dalem38  38219  dalem39  38220  dalem43  38224  dalem44  38225  dalem45  38226  dalem53  38234  dalem54  38235  dalem55  38236  dalem57  38238  dalem60  38241  snatpsubN  38259  linepsubN  38261  pmaple  38270  pmapat  38272  pmap1N  38276  pmapsub  38277  pmapglbx  38278  isline2  38283  linepmap  38284  isline3  38285  isline4N  38286  lneq2at  38287  lncvrelatN  38290  lncmp  38292  2lnat  38293  2atm2atN  38294  2llnma1b  38295  2llnma1  38296  2llnma3r  38297  cdlema1N  38300  cdlemblem  38302  cdlemb  38303  elpaddn0  38309  paddcom  38322  paddasslem2  38330  paddasslem5  38333  paddasslem12  38340  paddasslem13  38341  pmapjoin  38361  pmapjat1  38362  pmapjat2  38363  pmapjlln1  38364  atmod1i1  38366  atmod1i2  38368  llnmod1i2  38369  atmod2i1  38370  atmod2i2  38371  atmod3i1  38373  atmod3i2  38374  atmod4i1  38375  atmod4i2  38376  llnexchb2lem  38377  llnexchb2  38378  dalawlem2  38381  dalawlem3  38382  dalawlem5  38384  dalawlem6  38385  dalawlem7  38386  dalawlem8  38387  dalawlem11  38390  dalawlem12  38391  polval2N  38415  pol1N  38419  polatN  38440  2polatN  38441  paddatclN  38458  linepsubclN  38460  lhp2lt  38510  lhp0lt  38512  lhpexle2lem  38518  lhpexle3lem  38520  lhpjat2  38530  lhpj1  38531  lhpmcvr3  38534  lhpmcvr4N  38535  lhpmcvr5N  38536  lhpmcvr6N  38537  lhpmatb  38540  lhp2at0  38541  lhp2atnle  38542  lhp2at0nle  38544  lhprelat3N  38549  lhple  38551  lhpat4N  38553  lhpat3  38555  4atexlemtlw  38576  4atexlemc  38578  4atexlemnclw  38579  4atexlemcnd  38581  4atex2-0aOLDN  38587  lauteq  38604  ltrnid  38644  ltrnel  38648  ltrnat  38649  ltrncnvat  38650  ltrncnvel  38651  ltrncoval  38654  ltrncnv  38655  ltrn11at  38656  ltrneq2  38657  ltrneq  38658  idltrn  38659  trlval2  38672  trlcnv  38674  trljat1  38675  trljat2  38676  ltrnideq  38684  arglem1N  38699  cdlemc1  38700  cdlemc2  38701  cdlemc4  38703  cdlemc5  38704  cdlemc6  38705  cdlemd1  38707  cdlemd2  38708  cdlemd3  38709  cdlemd4  38710  cdlemd7  38713  cdleme0aa  38719  cdleme0b  38721  cdleme0c  38722  cdleme0cp  38723  cdleme0cq  38724  cdleme0e  38726  cdleme0fN  38727  cdleme1b  38735  cdleme1  38736  cdleme2  38737  cdleme3b  38738  cdleme3c  38739  cdleme3e  38741  cdleme3g  38743  cdleme3h  38744  cdleme3  38746  cdleme5  38749  cdleme7d  38755  cdleme7e  38756  cdleme7ga  38757  cdleme7  38758  cdleme8  38759  cdleme9  38762  cdleme10  38763  cdleme11c  38770  cdleme11e  38772  cdleme11fN  38773  cdleme11g  38774  cdleme11k  38777  cdleme11  38779  cdleme15b  38784  cdleme15  38787  cdleme16b  38788  cdleme17b  38796  cdleme17c  38797  cdlemednpq  38808  cdleme20zN  38810  cdleme19a  38812  cdleme20bN  38819  cdleme20d  38821  cdleme20j  38827  cdleme21c  38836  cdleme22aa  38848  cdleme22b  38850  cdleme22cN  38851  cdleme22d  38852  cdleme22e  38853  cdleme22eALTN  38854  cdleme23b  38859  cdleme23c  38860  cdleme27N  38878  cdleme28a  38879  cdleme30a  38887  cdlemefrs29pre00  38904  cdlemefrs29bpre0  38905  cdlemefrs29cpre1  38907  cdlemefrs32fva  38909  cdlemefrs32fva1  38910  cdlemefr32snb  38914  cdlemefs32snb  38924  cdleme32snb  38945  cdleme32fva  38946  cdleme32fva1  38947  cdleme32fvaw  38948  cdleme35a  38957  cdleme35fnpq  38958  cdleme35b  38959  cdleme35c  38960  cdleme35f  38963  cdleme42c  38981  cdleme42e  38988  cdleme42h  38991  cdleme42i  38992  cdleme42ke  38994  cdleme42keg  38995  cdleme42mgN  38997  cdleme17d4  39006  cdleme48fvg  39009  cdleme48bw  39011  cdlemeg46req  39038  cdleme50trn3  39062  cdlemf1  39070  cdlemf2  39071  trlord  39078  ltrniotacnvval  39091  cdlemg2fv2  39109  cdlemg2l  39112  cdlemg7fvbwN  39116  cdlemg4c  39121  cdlemg4  39126  cdlemg6c  39129  cdlemg8b  39137  cdlemg11b  39151  cdlemg13a  39160  cdlemg17a  39170  cdlemg17h  39177  cdlemg17  39186  cdlemg18b  39188  cdlemg19a  39192  cdlemg27a  39201  cdlemg27b  39205  cdlemg31a  39206  cdlemg31b  39207  cdlemg31d  39209  cdlemg33b0  39210  cdlemg33a  39215  cdlemg35  39222  trlcolem  39235  cdlemg42  39238  cdlemg44a  39240  cdlemg46  39244  cdlemh1  39324  cdlemh2  39325  cdlemh  39326  cdlemi1  39327  cdlemi  39329  cdlemk3  39342  cdlemk4  39343  cdlemkvcl  39351  cdlemk7  39357  cdlemk11  39358  cdlemk15  39364  cdlemk1u  39368  cdlemk7u  39379  cdlemk11u  39380  cdlemk37  39423  cdlemk39  39425  cdlemkid1  39431  cdlemkid2  39433  cdlemk48  39459  cdlemk50  39461  cdlemk51  39462  cdlemk52  39463  dia2dimlem1  39573  dia2dimlem2  39574  dia2dimlem3  39575  dia2dimlem5  39577  dia2dimlem7  39579  dia2dimlem9  39581  dia2dimlem10  39582  dia2dimlem12  39584  dia2dimlem13  39585  cdlemm10N  39627  cdlemn2  39704  cdlemn3  39706  cdlemn9  39714  cdlemn10  39715  dihjustlem  39725  dihord1  39727  dihord2pre2  39735  dihvalcqat  39748  dib2dim  39752  dih2dimb  39753  dih2dimbALTN  39754  dihord5apre  39771  dihglbcpreN  39809  dihmeetlem3N  39814  dihmeetlem6  39818  dihjatc1  39820  dihjatc2N  39821  dihjatc3  39822  dihmeetlem9N  39824  dihmeetlem10N  39825  dihmeetlem11N  39826  dihmeetlem13N  39828  dihmeetlem15N  39830  dihmeetlem16N  39831  dihmeetlem17N  39832  dihatexv2  39848  dihjatb  39925  dihjatc  39926  dihjatcclem1  39927  dihjatcclem2  39928  dihjatcclem4  39930  dihjat  39932  dihjat3  39941  dihjat5N  39946  dvh4dimat  39947
  Copyright terms: Public domain W3C validator