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

Theorem atbase 29531
Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 23032 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 3536 . . . 4  |-  ( P  e.  A  ->  -.  A  =  (/) )
2 atombase.a . . . . 5  |-  A  =  ( Atoms `  K )
32eqeq1i 2365 . . . 4  |-  ( A  =  (/)  <->  ( Atoms `  K
)  =  (/) )
41, 3sylnib 295 . . 3  |-  ( P  e.  A  ->  -.  ( Atoms `  K )  =  (/) )
5 fvprc 5599 . . 3  |-  ( -.  K  e.  _V  ->  (
Atoms `  K )  =  (/) )
64, 5nsyl2 119 . 2  |-  ( P  e.  A  ->  K  e.  _V )
7 atombase.b . . . 4  |-  B  =  ( Base `  K
)
8 eqid 2358 . . . 4  |-  ( 0.
`  K )  =  ( 0. `  K
)
9 eqid 2358 . . . 4  |-  (  <o  `  K )  =  ( 
<o  `  K )
107, 8, 9, 2isat 29528 . . 3  |-  ( K  e.  _V  ->  ( P  e.  A  <->  ( P  e.  B  /\  ( 0. `  K ) ( 
<o  `  K ) P ) ) )
1110simprbda 606 . 2  |-  ( ( K  e.  _V  /\  P  e.  A )  ->  P  e.  B )
126, 11mpancom 650 1  |-  ( P  e.  A  ->  P  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642    e. wcel 1710   _Vcvv 2864   (/)c0 3531   class class class wbr 4102   ` cfv 5334   Basecbs 13239   0.cp0 14236    <o ccvr 29504   Atomscatm 29505
This theorem is referenced by:  atssbase  29532  0ltat  29533  leatb  29534  meetat  29538  atnle0  29551  atlen0  29552  atcmp  29553  atcvreq0  29556  atncvrN  29557  atnle  29559  atnem0  29560  atlatmstc  29561  atlatle  29562  cvlexch2  29571  cvlexchb1  29572  cvlexchb2  29573  cvlatexchb1  29576  cvlatexchb2  29577  cvlatexch1  29578  cvlatexch2  29579  cvlatexch3  29580  cvlcvr1  29581  cvlcvrp  29582  cvlatcvr1  29583  cvlatcvr2  29584  cvlsupr2  29585  cvlsupr7  29590  cvlsupr8  29591  hlatjcl  29608  hlatjcom  29609  hlatjidm  29610  hlatjass  29611  hlatj32  29613  hlatj4  29615  hlatlej1  29616  atnlej1  29620  atnlej2  29621  hlrelat5N  29642  hlrelat  29643  hlrelat2  29644  exatleN  29645  cvr2N  29652  hlrelat3  29653  cvrval3  29654  cvrval5  29656  cvrexchlem  29660  cvratlem  29662  cvrat  29663  atcvr0eq  29667  lnnat  29668  cvrat2  29670  atcvrneN  29671  atcvrj1  29672  atcvrj2b  29673  atltcvr  29676  atle  29677  atlelt  29679  2atlt  29680  atexchcvrN  29681  cvrat3  29683  cvrat4  29684  cvrat42  29685  2atjm  29686  atbtwn  29687  3noncolr2  29690  4noncolr3  29694  athgt  29697  3dim0  29698  3dimlem3a  29701  3dimlem3OLDN  29703  3dimlem4a  29704  3dimlem4OLDN  29706  3dim3  29710  2dim  29711  1cvratex  29714  1cvrjat  29716  1cvrat  29717  ps-1  29718  ps-2  29719  hlatexch3N  29721  hlatexch4  29722  ps-2b  29723  3atlem1  29724  3atlem2  29725  3atlem4  29727  3atlem5  29728  3atlem6  29729  3at  29731  islln3  29751  llnnleat  29754  llnn0  29757  llnle  29759  llnexatN  29762  llncmp  29763  2llnmat  29765  2at0mat0  29766  2atm  29768  ps-2c  29769  lplni2  29778  lplnle  29781  lplnnle2at  29782  lplnn0N  29788  islpln2a  29789  2atmat  29802  lplnexllnN  29805  2llnjaN  29807  2llnm4  29811  2llnmeqat  29812  lvoli3  29818  islvol5  29820  lvoli2  29822  lvolnle3at  29823  3atnelvolN  29827  lvoln0N  29832  islvol2aN  29833  4atlem3  29837  4atlem3a  29838  4atlem3b  29839  4atlem4a  29840  4atlem4b  29841  4atlem4c  29842  4atlem4d  29843  4atlem9  29844  4atlem10a  29845  4atlem10  29847  4atlem11a  29848  4atlem11b  29849  4atlem11  29850  4atlem12a  29851  4atlem12b  29852  4atlem12  29853  4at2  29855  lplncvrlvol2  29856  2lplnja  29860  dalempeb  29880  dalemqeb  29881  dalemreb  29882  dalemseb  29883  dalemteb  29884  dalemueb  29885  dalem3  29905  dalem16  29920  dalemcceb  29930  dalem21  29935  dalem25  29939  dalem38  29951  dalem39  29952  dalem43  29956  dalem44  29957  dalem45  29958  dalem53  29966  dalem54  29967  dalem55  29968  dalem57  29970  dalem60  29973  snatpsubN  29991  linepsubN  29993  pmaple  30002  pmapat  30004  pmap1N  30008  pmapsub  30009  pmapglbx  30010  isline2  30015  linepmap  30016  isline3  30017  isline4N  30018  lneq2at  30019  lncvrelatN  30022  lncmp  30024  2lnat  30025  2atm2atN  30026  2llnma1b  30027  2llnma1  30028  2llnma3r  30029  cdlema1N  30032  cdlemblem  30034  cdlemb  30035  elpaddn0  30041  paddcom  30054  paddasslem2  30062  paddasslem5  30065  paddasslem12  30072  paddasslem13  30073  pmapjoin  30093  pmapjat1  30094  pmapjat2  30095  pmapjlln1  30096  atmod1i1  30098  atmod1i2  30100  llnmod1i2  30101  atmod2i1  30102  atmod2i2  30103  atmod3i1  30105  atmod3i2  30106  atmod4i1  30107  atmod4i2  30108  llnexchb2lem  30109  llnexchb2  30110  dalawlem2  30113  dalawlem3  30114  dalawlem5  30116  dalawlem6  30117  dalawlem7  30118  dalawlem8  30119  dalawlem11  30122  dalawlem12  30123  polval2N  30147  pol1N  30151  polatN  30172  2polatN  30173  paddatclN  30190  linepsubclN  30192  lhp2lt  30242  lhp0lt  30244  lhpexle2lem  30250  lhpexle3lem  30252  lhpjat2  30262  lhpj1  30263  lhpmcvr3  30266  lhpmcvr4N  30267  lhpmcvr5N  30268  lhpmcvr6N  30269  lhpmatb  30272  lhp2at0  30273  lhp2atnle  30274  lhp2at0nle  30276  lhprelat3N  30281  lhple  30283  lhpat4N  30285  lhpat3  30287  4atexlemtlw  30308  4atexlemc  30310  4atexlemnclw  30311  4atexlemcnd  30313  4atex2-0aOLDN  30319  lauteq  30336  ltrnid  30376  ltrnel  30380  ltrnat  30381  ltrncnvat  30382  ltrncnvel  30383  ltrncoval  30386  ltrncnv  30387  ltrn11at  30388  ltrneq2  30389  ltrneq  30390  idltrn  30391  ltrnmw  30392  trlval2  30404  trlcnv  30406  trljat1  30407  trljat2  30408  ltrnideq  30416  arglem1N  30431  cdlemc1  30432  cdlemc2  30433  cdlemc4  30435  cdlemc5  30436  cdlemc6  30437  cdlemd1  30439  cdlemd2  30440  cdlemd3  30441  cdlemd4  30442  cdlemd7  30445  cdleme0aa  30451  cdleme0b  30453  cdleme0c  30454  cdleme0cp  30455  cdleme0cq  30456  cdleme0e  30458  cdleme0fN  30459  cdleme1b  30467  cdleme1  30468  cdleme2  30469  cdleme3b  30470  cdleme3c  30471  cdleme3e  30473  cdleme3g  30475  cdleme3h  30476  cdleme3  30478  cdleme5  30481  cdleme7d  30487  cdleme7e  30488  cdleme7ga  30489  cdleme7  30490  cdleme8  30491  cdleme9  30494  cdleme10  30495  cdleme11c  30502  cdleme11e  30504  cdleme11fN  30505  cdleme11g  30506  cdleme11k  30509  cdleme11  30511  cdleme15b  30516  cdleme15  30519  cdleme16b  30520  cdleme17b  30528  cdleme17c  30529  cdlemednpq  30540  cdleme20zN  30542  cdleme20y  30543  cdleme19a  30544  cdleme20bN  30551  cdleme20d  30553  cdleme20j  30559  cdleme21c  30568  cdleme22aa  30580  cdleme22b  30582  cdleme22cN  30583  cdleme22d  30584  cdleme22e  30585  cdleme22eALTN  30586  cdleme23b  30591  cdleme23c  30592  cdleme27N  30610  cdleme28a  30611  cdleme30a  30619  cdlemefrs29pre00  30636  cdlemefrs29bpre0  30637  cdlemefrs29cpre1  30639  cdlemefrs32fva  30641  cdlemefrs32fva1  30642  cdlemefr32snb  30646  cdlemefs32snb  30656  cdleme32snb  30677  cdleme32fva  30678  cdleme32fva1  30679  cdleme32fvaw  30680  cdleme35a  30689  cdleme35fnpq  30690  cdleme35b  30691  cdleme35c  30692  cdleme35f  30695  cdleme42c  30713  cdleme42e  30720  cdleme42h  30723  cdleme42i  30724  cdleme42ke  30726  cdleme42keg  30727  cdleme42mgN  30729  cdleme17d4  30738  cdleme48fvg  30741  cdleme48bw  30743  cdlemeg46req  30770  cdleme50trn3  30794  cdlemf1  30802  cdlemf2  30803  trlord  30810  ltrniotacnvval  30823  cdlemg2fv2  30841  cdlemg2l  30844  cdlemg7fvbwN  30848  cdlemg4c  30853  cdlemg4  30858  cdlemg6c  30861  cdlemg8b  30869  cdlemg11b  30883  cdlemg13a  30892  cdlemg17a  30902  cdlemg17h  30909  cdlemg17  30918  cdlemg18b  30920  cdlemg19a  30924  cdlemg27a  30933  cdlemg27b  30937  cdlemg31a  30938  cdlemg31b  30939  cdlemg31d  30941  cdlemg33b0  30942  cdlemg33a  30947  cdlemg35  30954  trlcolem  30967  cdlemg42  30970  cdlemg44a  30972  cdlemg46  30976  cdlemh1  31056  cdlemh2  31057  cdlemh  31058  cdlemi1  31059  cdlemi  31061  cdlemk3  31074  cdlemk4  31075  cdlemkvcl  31083  cdlemk7  31089  cdlemk11  31090  cdlemk15  31096  cdlemk1u  31100  cdlemk7u  31111  cdlemk11u  31112  cdlemk37  31155  cdlemk39  31157  cdlemkid1  31163  cdlemkid2  31165  cdlemk48  31191  cdlemk50  31193  cdlemk51  31194  cdlemk52  31195  dia2dimlem1  31306  dia2dimlem2  31307  dia2dimlem3  31308  dia2dimlem5  31310  dia2dimlem7  31312  dia2dimlem9  31314  dia2dimlem10  31315  dia2dimlem12  31317  dia2dimlem13  31318  cdlemm10N  31360  cdlemn2  31437  cdlemn3  31439  cdlemn9  31447  cdlemn10  31448  dihjustlem  31458  dihord1  31460  dihord2pre2  31468  dihvalcqat  31481  dib2dim  31485  dih2dimb  31486  dih2dimbALTN  31487  dihord5apre  31504  dihglbcpreN  31542  dihmeetlem3N  31547  dihmeetlem6  31551  dihjatc1  31553  dihjatc2N  31554  dihjatc3  31555  dihmeetlem9N  31557  dihmeetlem10N  31558  dihmeetlem11N  31559  dihmeetlem13N  31561  dihmeetlem15N  31563  dihmeetlem16N  31564  dihmeetlem17N  31565  dihatexv2  31581  dihjatb  31658  dihjatc  31659  dihjatcclem1  31660  dihjatcclem2  31661  dihjatcclem4  31663  dihjat  31665  dihjat3  31674  dihjat5N  31679  dvh4dimat  31680
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4220  ax-nul 4228  ax-pow 4267  ax-pr 4293
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3907  df-br 4103  df-opab 4157  df-mpt 4158  df-id 4388  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-iota 5298  df-fun 5336  df-fv 5342  df-ats 29509
  Copyright terms: Public domain W3C validator