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

Theorem atbase 30087
Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 23847 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 3633 . . . 4  |-  ( P  e.  A  ->  -.  A  =  (/) )
2 atombase.a . . . . 5  |-  A  =  ( Atoms `  K )
32eqeq1i 2443 . . . 4  |-  ( A  =  (/)  <->  ( Atoms `  K
)  =  (/) )
41, 3sylnib 296 . . 3  |-  ( P  e.  A  ->  -.  ( Atoms `  K )  =  (/) )
5 fvprc 5722 . . 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 2436 . . . 4  |-  ( 0.
`  K )  =  ( 0. `  K
)
9 eqid 2436 . . . 4  |-  (  <o  `  K )  =  ( 
<o  `  K )
107, 8, 9, 2isat 30084 . . 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 1652    e. wcel 1725   _Vcvv 2956   (/)c0 3628   class class class wbr 4212   ` cfv 5454   Basecbs 13469   0.cp0 14466    <o ccvr 30060   Atomscatm 30061
This theorem is referenced by:  atssbase  30088  0ltat  30089  leatb  30090  meetat  30094  atnle0  30107  atlen0  30108  atcmp  30109  atcvreq0  30112  atncvrN  30113  atnle  30115  atnem0  30116  atlatmstc  30117  atlatle  30118  cvlexch2  30127  cvlexchb1  30128  cvlexchb2  30129  cvlatexchb1  30132  cvlatexchb2  30133  cvlatexch1  30134  cvlatexch2  30135  cvlatexch3  30136  cvlcvr1  30137  cvlcvrp  30138  cvlatcvr1  30139  cvlatcvr2  30140  cvlsupr2  30141  cvlsupr7  30146  cvlsupr8  30147  hlatjcl  30164  hlatjcom  30165  hlatjidm  30166  hlatjass  30167  hlatj32  30169  hlatj4  30171  hlatlej1  30172  atnlej1  30176  atnlej2  30177  hlrelat5N  30198  hlrelat  30199  hlrelat2  30200  exatleN  30201  cvr2N  30208  hlrelat3  30209  cvrval3  30210  cvrval5  30212  cvrexchlem  30216  cvratlem  30218  cvrat  30219  atcvr0eq  30223  lnnat  30224  cvrat2  30226  atcvrneN  30227  atcvrj1  30228  atcvrj2b  30229  atltcvr  30232  atle  30233  atlelt  30235  2atlt  30236  atexchcvrN  30237  cvrat3  30239  cvrat4  30240  cvrat42  30241  2atjm  30242  atbtwn  30243  3noncolr2  30246  4noncolr3  30250  athgt  30253  3dim0  30254  3dimlem3a  30257  3dimlem3OLDN  30259  3dimlem4a  30260  3dimlem4OLDN  30262  3dim3  30266  2dim  30267  1cvratex  30270  1cvrjat  30272  1cvrat  30273  ps-1  30274  ps-2  30275  hlatexch3N  30277  hlatexch4  30278  ps-2b  30279  3atlem1  30280  3atlem2  30281  3atlem4  30283  3atlem5  30284  3atlem6  30285  3at  30287  islln3  30307  llnnleat  30310  llnn0  30313  llnle  30315  llnexatN  30318  llncmp  30319  2llnmat  30321  2at0mat0  30322  2atm  30324  ps-2c  30325  lplni2  30334  lplnle  30337  lplnnle2at  30338  lplnn0N  30344  islpln2a  30345  2atmat  30358  lplnexllnN  30361  2llnjaN  30363  2llnm4  30367  2llnmeqat  30368  lvoli3  30374  islvol5  30376  lvoli2  30378  lvolnle3at  30379  3atnelvolN  30383  lvoln0N  30388  islvol2aN  30389  4atlem3  30393  4atlem3a  30394  4atlem3b  30395  4atlem4a  30396  4atlem4b  30397  4atlem4c  30398  4atlem4d  30399  4atlem9  30400  4atlem10a  30401  4atlem10  30403  4atlem11a  30404  4atlem11b  30405  4atlem11  30406  4atlem12a  30407  4atlem12b  30408  4atlem12  30409  4at2  30411  lplncvrlvol2  30412  2lplnja  30416  dalempeb  30436  dalemqeb  30437  dalemreb  30438  dalemseb  30439  dalemteb  30440  dalemueb  30441  dalem3  30461  dalem16  30476  dalemcceb  30486  dalem21  30491  dalem25  30495  dalem38  30507  dalem39  30508  dalem43  30512  dalem44  30513  dalem45  30514  dalem53  30522  dalem54  30523  dalem55  30524  dalem57  30526  dalem60  30529  snatpsubN  30547  linepsubN  30549  pmaple  30558  pmapat  30560  pmap1N  30564  pmapsub  30565  pmapglbx  30566  isline2  30571  linepmap  30572  isline3  30573  isline4N  30574  lneq2at  30575  lncvrelatN  30578  lncmp  30580  2lnat  30581  2atm2atN  30582  2llnma1b  30583  2llnma1  30584  2llnma3r  30585  cdlema1N  30588  cdlemblem  30590  cdlemb  30591  elpaddn0  30597  paddcom  30610  paddasslem2  30618  paddasslem5  30621  paddasslem12  30628  paddasslem13  30629  pmapjoin  30649  pmapjat1  30650  pmapjat2  30651  pmapjlln1  30652  atmod1i1  30654  atmod1i2  30656  llnmod1i2  30657  atmod2i1  30658  atmod2i2  30659  atmod3i1  30661  atmod3i2  30662  atmod4i1  30663  atmod4i2  30664  llnexchb2lem  30665  llnexchb2  30666  dalawlem2  30669  dalawlem3  30670  dalawlem5  30672  dalawlem6  30673  dalawlem7  30674  dalawlem8  30675  dalawlem11  30678  dalawlem12  30679  polval2N  30703  pol1N  30707  polatN  30728  2polatN  30729  paddatclN  30746  linepsubclN  30748  lhp2lt  30798  lhp0lt  30800  lhpexle2lem  30806  lhpexle3lem  30808  lhpjat2  30818  lhpj1  30819  lhpmcvr3  30822  lhpmcvr4N  30823  lhpmcvr5N  30824  lhpmcvr6N  30825  lhpmatb  30828  lhp2at0  30829  lhp2atnle  30830  lhp2at0nle  30832  lhprelat3N  30837  lhple  30839  lhpat4N  30841  lhpat3  30843  4atexlemtlw  30864  4atexlemc  30866  4atexlemnclw  30867  4atexlemcnd  30869  4atex2-0aOLDN  30875  lauteq  30892  ltrnid  30932  ltrnel  30936  ltrnat  30937  ltrncnvat  30938  ltrncnvel  30939  ltrncoval  30942  ltrncnv  30943  ltrn11at  30944  ltrneq2  30945  ltrneq  30946  idltrn  30947  ltrnmw  30948  trlval2  30960  trlcnv  30962  trljat1  30963  trljat2  30964  ltrnideq  30972  arglem1N  30987  cdlemc1  30988  cdlemc2  30989  cdlemc4  30991  cdlemc5  30992  cdlemc6  30993  cdlemd1  30995  cdlemd2  30996  cdlemd3  30997  cdlemd4  30998  cdlemd7  31001  cdleme0aa  31007  cdleme0b  31009  cdleme0c  31010  cdleme0cp  31011  cdleme0cq  31012  cdleme0e  31014  cdleme0fN  31015  cdleme1b  31023  cdleme1  31024  cdleme2  31025  cdleme3b  31026  cdleme3c  31027  cdleme3e  31029  cdleme3g  31031  cdleme3h  31032  cdleme3  31034  cdleme5  31037  cdleme7d  31043  cdleme7e  31044  cdleme7ga  31045  cdleme7  31046  cdleme8  31047  cdleme9  31050  cdleme10  31051  cdleme11c  31058  cdleme11e  31060  cdleme11fN  31061  cdleme11g  31062  cdleme11k  31065  cdleme11  31067  cdleme15b  31072  cdleme15  31075  cdleme16b  31076  cdleme17b  31084  cdleme17c  31085  cdlemednpq  31096  cdleme20zN  31098  cdleme20y  31099  cdleme19a  31100  cdleme20bN  31107  cdleme20d  31109  cdleme20j  31115  cdleme21c  31124  cdleme22aa  31136  cdleme22b  31138  cdleme22cN  31139  cdleme22d  31140  cdleme22e  31141  cdleme22eALTN  31142  cdleme23b  31147  cdleme23c  31148  cdleme27N  31166  cdleme28a  31167  cdleme30a  31175  cdlemefrs29pre00  31192  cdlemefrs29bpre0  31193  cdlemefrs29cpre1  31195  cdlemefrs32fva  31197  cdlemefrs32fva1  31198  cdlemefr32snb  31202  cdlemefs32snb  31212  cdleme32snb  31233  cdleme32fva  31234  cdleme32fva1  31235  cdleme32fvaw  31236  cdleme35a  31245  cdleme35fnpq  31246  cdleme35b  31247  cdleme35c  31248  cdleme35f  31251  cdleme42c  31269  cdleme42e  31276  cdleme42h  31279  cdleme42i  31280  cdleme42ke  31282  cdleme42keg  31283  cdleme42mgN  31285  cdleme17d4  31294  cdleme48fvg  31297  cdleme48bw  31299  cdlemeg46req  31326  cdleme50trn3  31350  cdlemf1  31358  cdlemf2  31359  trlord  31366  ltrniotacnvval  31379  cdlemg2fv2  31397  cdlemg2l  31400  cdlemg7fvbwN  31404  cdlemg4c  31409  cdlemg4  31414  cdlemg6c  31417  cdlemg8b  31425  cdlemg11b  31439  cdlemg13a  31448  cdlemg17a  31458  cdlemg17h  31465  cdlemg17  31474  cdlemg18b  31476  cdlemg19a  31480  cdlemg27a  31489  cdlemg27b  31493  cdlemg31a  31494  cdlemg31b  31495  cdlemg31d  31497  cdlemg33b0  31498  cdlemg33a  31503  cdlemg35  31510  trlcolem  31523  cdlemg42  31526  cdlemg44a  31528  cdlemg46  31532  cdlemh1  31612  cdlemh2  31613  cdlemh  31614  cdlemi1  31615  cdlemi  31617  cdlemk3  31630  cdlemk4  31631  cdlemkvcl  31639  cdlemk7  31645  cdlemk11  31646  cdlemk15  31652  cdlemk1u  31656  cdlemk7u  31667  cdlemk11u  31668  cdlemk37  31711  cdlemk39  31713  cdlemkid1  31719  cdlemkid2  31721  cdlemk48  31747  cdlemk50  31749  cdlemk51  31750  cdlemk52  31751  dia2dimlem1  31862  dia2dimlem2  31863  dia2dimlem3  31864  dia2dimlem5  31866  dia2dimlem7  31868  dia2dimlem9  31870  dia2dimlem10  31871  dia2dimlem12  31873  dia2dimlem13  31874  cdlemm10N  31916  cdlemn2  31993  cdlemn3  31995  cdlemn9  32003  cdlemn10  32004  dihjustlem  32014  dihord1  32016  dihord2pre2  32024  dihvalcqat  32037  dib2dim  32041  dih2dimb  32042  dih2dimbALTN  32043  dihord5apre  32060  dihglbcpreN  32098  dihmeetlem3N  32103  dihmeetlem6  32107  dihjatc1  32109  dihjatc2N  32110  dihjatc3  32111  dihmeetlem9N  32113  dihmeetlem10N  32114  dihmeetlem11N  32115  dihmeetlem13N  32117  dihmeetlem15N  32119  dihmeetlem16N  32120  dihmeetlem17N  32121  dihatexv2  32137  dihjatb  32214  dihjatc  32215  dihjatcclem1  32216  dihjatcclem2  32217  dihjatcclem4  32219  dihjat  32221  dihjat3  32230  dihjat5N  32235  dvh4dimat  32236
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-sbc 3162  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-opab 4267  df-mpt 4268  df-id 4498  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-iota 5418  df-fun 5456  df-fv 5462  df-ats 30065
  Copyright terms: Public domain W3C validator