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

Theorem atbase 29776
Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 23804 analog.) (Contributed by NM, 10-Oct-2011.)
Hypotheses
Ref Expression
atombase.b  |-  B  =  ( Base `  K
)
atombase.a  |-  A  =  ( Atoms `  K )
Assertion
Ref Expression
atbase  |-  ( P  e.  A  ->  P  e.  B )

Proof of Theorem atbase
StepHypRef Expression
1 n0i 3597 . . . 4  |-  ( P  e.  A  ->  -.  A  =  (/) )
2 atombase.a . . . . 5  |-  A  =  ( Atoms `  K )
32eqeq1i 2415 . . . 4  |-  ( A  =  (/)  <->  ( Atoms `  K
)  =  (/) )
41, 3sylnib 296 . . 3  |-  ( P  e.  A  ->  -.  ( Atoms `  K )  =  (/) )
5 fvprc 5685 . . 3  |-  ( -.  K  e.  _V  ->  (
Atoms `  K )  =  (/) )
64, 5nsyl2 121 . 2  |-  ( P  e.  A  ->  K  e.  _V )
7 atombase.b . . . 4  |-  B  =  ( Base `  K
)
8 eqid 2408 . . . 4  |-  ( 0.
`  K )  =  ( 0. `  K
)
9 eqid 2408 . . . 4  |-  (  <o  `  K )  =  ( 
<o  `  K )
107, 8, 9, 2isat 29773 . . 3  |-  ( K  e.  _V  ->  ( P  e.  A  <->  ( P  e.  B  /\  ( 0. `  K ) ( 
<o  `  K ) P ) ) )
1110simprbda 607 . 2  |-  ( ( K  e.  _V  /\  P  e.  A )  ->  P  e.  B )
126, 11mpancom 651 1  |-  ( P  e.  A  ->  P  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721   _Vcvv 2920   (/)c0 3592   class class class wbr 4176   ` cfv 5417   Basecbs 13428   0.cp0 14425    <o ccvr 29749   Atomscatm 29750
This theorem is referenced by:  atssbase  29777  0ltat  29778  leatb  29779  meetat  29783  atnle0  29796  atlen0  29797  atcmp  29798  atcvreq0  29801  atncvrN  29802  atnle  29804  atnem0  29805  atlatmstc  29806  atlatle  29807  cvlexch2  29816  cvlexchb1  29817  cvlexchb2  29818  cvlatexchb1  29821  cvlatexchb2  29822  cvlatexch1  29823  cvlatexch2  29824  cvlatexch3  29825  cvlcvr1  29826  cvlcvrp  29827  cvlatcvr1  29828  cvlatcvr2  29829  cvlsupr2  29830  cvlsupr7  29835  cvlsupr8  29836  hlatjcl  29853  hlatjcom  29854  hlatjidm  29855  hlatjass  29856  hlatj32  29858  hlatj4  29860  hlatlej1  29861  atnlej1  29865  atnlej2  29866  hlrelat5N  29887  hlrelat  29888  hlrelat2  29889  exatleN  29890  cvr2N  29897  hlrelat3  29898  cvrval3  29899  cvrval5  29901  cvrexchlem  29905  cvratlem  29907  cvrat  29908  atcvr0eq  29912  lnnat  29913  cvrat2  29915  atcvrneN  29916  atcvrj1  29917  atcvrj2b  29918  atltcvr  29921  atle  29922  atlelt  29924  2atlt  29925  atexchcvrN  29926  cvrat3  29928  cvrat4  29929  cvrat42  29930  2atjm  29931  atbtwn  29932  3noncolr2  29935  4noncolr3  29939  athgt  29942  3dim0  29943  3dimlem3a  29946  3dimlem3OLDN  29948  3dimlem4a  29949  3dimlem4OLDN  29951  3dim3  29955  2dim  29956  1cvratex  29959  1cvrjat  29961  1cvrat  29962  ps-1  29963  ps-2  29964  hlatexch3N  29966  hlatexch4  29967  ps-2b  29968  3atlem1  29969  3atlem2  29970  3atlem4  29972  3atlem5  29973  3atlem6  29974  3at  29976  islln3  29996  llnnleat  29999  llnn0  30002  llnle  30004  llnexatN  30007  llncmp  30008  2llnmat  30010  2at0mat0  30011  2atm  30013  ps-2c  30014  lplni2  30023  lplnle  30026  lplnnle2at  30027  lplnn0N  30033  islpln2a  30034  2atmat  30047  lplnexllnN  30050  2llnjaN  30052  2llnm4  30056  2llnmeqat  30057  lvoli3  30063  islvol5  30065  lvoli2  30067  lvolnle3at  30068  3atnelvolN  30072  lvoln0N  30077  islvol2aN  30078  4atlem3  30082  4atlem3a  30083  4atlem3b  30084  4atlem4a  30085  4atlem4b  30086  4atlem4c  30087  4atlem4d  30088  4atlem9  30089  4atlem10a  30090  4atlem10  30092  4atlem11a  30093  4atlem11b  30094  4atlem11  30095  4atlem12a  30096  4atlem12b  30097  4atlem12  30098  4at2  30100  lplncvrlvol2  30101  2lplnja  30105  dalempeb  30125  dalemqeb  30126  dalemreb  30127  dalemseb  30128  dalemteb  30129  dalemueb  30130  dalem3  30150  dalem16  30165  dalemcceb  30175  dalem21  30180  dalem25  30184  dalem38  30196  dalem39  30197  dalem43  30201  dalem44  30202  dalem45  30203  dalem53  30211  dalem54  30212  dalem55  30213  dalem57  30215  dalem60  30218  snatpsubN  30236  linepsubN  30238  pmaple  30247  pmapat  30249  pmap1N  30253  pmapsub  30254  pmapglbx  30255  isline2  30260  linepmap  30261  isline3  30262  isline4N  30263  lneq2at  30264  lncvrelatN  30267  lncmp  30269  2lnat  30270  2atm2atN  30271  2llnma1b  30272  2llnma1  30273  2llnma3r  30274  cdlema1N  30277  cdlemblem  30279  cdlemb  30280  elpaddn0  30286  paddcom  30299  paddasslem2  30307  paddasslem5  30310  paddasslem12  30317  paddasslem13  30318  pmapjoin  30338  pmapjat1  30339  pmapjat2  30340  pmapjlln1  30341  atmod1i1  30343  atmod1i2  30345  llnmod1i2  30346  atmod2i1  30347  atmod2i2  30348  atmod3i1  30350  atmod3i2  30351  atmod4i1  30352  atmod4i2  30353  llnexchb2lem  30354  llnexchb2  30355  dalawlem2  30358  dalawlem3  30359  dalawlem5  30361  dalawlem6  30362  dalawlem7  30363  dalawlem8  30364  dalawlem11  30367  dalawlem12  30368  polval2N  30392  pol1N  30396  polatN  30417  2polatN  30418  paddatclN  30435  linepsubclN  30437  lhp2lt  30487  lhp0lt  30489  lhpexle2lem  30495  lhpexle3lem  30497  lhpjat2  30507  lhpj1  30508  lhpmcvr3  30511  lhpmcvr4N  30512  lhpmcvr5N  30513  lhpmcvr6N  30514  lhpmatb  30517  lhp2at0  30518  lhp2atnle  30519  lhp2at0nle  30521  lhprelat3N  30526  lhple  30528  lhpat4N  30530  lhpat3  30532  4atexlemtlw  30553  4atexlemc  30555  4atexlemnclw  30556  4atexlemcnd  30558  4atex2-0aOLDN  30564  lauteq  30581  ltrnid  30621  ltrnel  30625  ltrnat  30626  ltrncnvat  30627  ltrncnvel  30628  ltrncoval  30631  ltrncnv  30632  ltrn11at  30633  ltrneq2  30634  ltrneq  30635  idltrn  30636  ltrnmw  30637  trlval2  30649  trlcnv  30651  trljat1  30652  trljat2  30653  ltrnideq  30661  arglem1N  30676  cdlemc1  30677  cdlemc2  30678  cdlemc4  30680  cdlemc5  30681  cdlemc6  30682  cdlemd1  30684  cdlemd2  30685  cdlemd3  30686  cdlemd4  30687  cdlemd7  30690  cdleme0aa  30696  cdleme0b  30698  cdleme0c  30699  cdleme0cp  30700  cdleme0cq  30701  cdleme0e  30703  cdleme0fN  30704  cdleme1b  30712  cdleme1  30713  cdleme2  30714  cdleme3b  30715  cdleme3c  30716  cdleme3e  30718  cdleme3g  30720  cdleme3h  30721  cdleme3  30723  cdleme5  30726  cdleme7d  30732  cdleme7e  30733  cdleme7ga  30734  cdleme7  30735  cdleme8  30736  cdleme9  30739  cdleme10  30740  cdleme11c  30747  cdleme11e  30749  cdleme11fN  30750  cdleme11g  30751  cdleme11k  30754  cdleme11  30756  cdleme15b  30761  cdleme15  30764  cdleme16b  30765  cdleme17b  30773  cdleme17c  30774  cdlemednpq  30785  cdleme20zN  30787  cdleme20y  30788  cdleme19a  30789  cdleme20bN  30796  cdleme20d  30798  cdleme20j  30804  cdleme21c  30813  cdleme22aa  30825  cdleme22b  30827  cdleme22cN  30828  cdleme22d  30829  cdleme22e  30830  cdleme22eALTN  30831  cdleme23b  30836  cdleme23c  30837  cdleme27N  30855  cdleme28a  30856  cdleme30a  30864  cdlemefrs29pre00  30881  cdlemefrs29bpre0  30882  cdlemefrs29cpre1  30884  cdlemefrs32fva  30886  cdlemefrs32fva1  30887  cdlemefr32snb  30891  cdlemefs32snb  30901  cdleme32snb  30922  cdleme32fva  30923  cdleme32fva1  30924  cdleme32fvaw  30925  cdleme35a  30934  cdleme35fnpq  30935  cdleme35b  30936  cdleme35c  30937  cdleme35f  30940  cdleme42c  30958  cdleme42e  30965  cdleme42h  30968  cdleme42i  30969  cdleme42ke  30971  cdleme42keg  30972  cdleme42mgN  30974  cdleme17d4  30983  cdleme48fvg  30986  cdleme48bw  30988  cdlemeg46req  31015  cdleme50trn3  31039  cdlemf1  31047  cdlemf2  31048  trlord  31055  ltrniotacnvval  31068  cdlemg2fv2  31086  cdlemg2l  31089  cdlemg7fvbwN  31093  cdlemg4c  31098  cdlemg4  31103  cdlemg6c  31106  cdlemg8b  31114  cdlemg11b  31128  cdlemg13a  31137  cdlemg17a  31147  cdlemg17h  31154  cdlemg17  31163  cdlemg18b  31165  cdlemg19a  31169  cdlemg27a  31178  cdlemg27b  31182  cdlemg31a  31183  cdlemg31b  31184  cdlemg31d  31186  cdlemg33b0  31187  cdlemg33a  31192  cdlemg35  31199  trlcolem  31212  cdlemg42  31215  cdlemg44a  31217  cdlemg46  31221  cdlemh1  31301  cdlemh2  31302  cdlemh  31303  cdlemi1  31304  cdlemi  31306  cdlemk3  31319  cdlemk4  31320  cdlemkvcl  31328  cdlemk7  31334  cdlemk11  31335  cdlemk15  31341  cdlemk1u  31345  cdlemk7u  31356  cdlemk11u  31357  cdlemk37  31400  cdlemk39  31402  cdlemkid1  31408  cdlemkid2  31410  cdlemk48  31436  cdlemk50  31438  cdlemk51  31439  cdlemk52  31440  dia2dimlem1  31551  dia2dimlem2  31552  dia2dimlem3  31553  dia2dimlem5  31555  dia2dimlem7  31557  dia2dimlem9  31559  dia2dimlem10  31560  dia2dimlem12  31562  dia2dimlem13  31563  cdlemm10N  31605  cdlemn2  31682  cdlemn3  31684  cdlemn9  31692  cdlemn10  31693  dihjustlem  31703  dihord1  31705  dihord2pre2  31713  dihvalcqat  31726  dib2dim  31730  dih2dimb  31731  dih2dimbALTN  31732  dihord5apre  31749  dihglbcpreN  31787  dihmeetlem3N  31792  dihmeetlem6  31796  dihjatc1  31798  dihjatc2N  31799  dihjatc3  31800  dihmeetlem9N  31802  dihmeetlem10N  31803  dihmeetlem11N  31804  dihmeetlem13N  31806  dihmeetlem15N  31808  dihmeetlem16N  31809  dihmeetlem17N  31810  dihatexv2  31826  dihjatb  31903  dihjatc  31904  dihjatcclem1  31905  dihjatcclem2  31906  dihjatcclem4  31908  dihjat  31910  dihjat3  31919  dihjat5N  31924  dvh4dimat  31925
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-sbc 3126  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-br 4177  df-opab 4231  df-mpt 4232  df-id 4462  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-iota 5381  df-fun 5419  df-fv 5425  df-ats 29754
  Copyright terms: Public domain W3C validator