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

Theorem atbase 29772
Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 23800 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 3593 . . . 4  |-  ( P  e.  A  ->  -.  A  =  (/) )
2 atombase.a . . . . 5  |-  A  =  ( Atoms `  K )
32eqeq1i 2411 . . . 4  |-  ( A  =  (/)  <->  ( Atoms `  K
)  =  (/) )
41, 3sylnib 296 . . 3  |-  ( P  e.  A  ->  -.  ( Atoms `  K )  =  (/) )
5 fvprc 5681 . . 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 2404 . . . 4  |-  ( 0.
`  K )  =  ( 0. `  K
)
9 eqid 2404 . . . 4  |-  (  <o  `  K )  =  ( 
<o  `  K )
107, 8, 9, 2isat 29769 . . 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 2916   (/)c0 3588   class class class wbr 4172   ` cfv 5413   Basecbs 13424   0.cp0 14421    <o ccvr 29745   Atomscatm 29746
This theorem is referenced by:  atssbase  29773  0ltat  29774  leatb  29775  meetat  29779  atnle0  29792  atlen0  29793  atcmp  29794  atcvreq0  29797  atncvrN  29798  atnle  29800  atnem0  29801  atlatmstc  29802  atlatle  29803  cvlexch2  29812  cvlexchb1  29813  cvlexchb2  29814  cvlatexchb1  29817  cvlatexchb2  29818  cvlatexch1  29819  cvlatexch2  29820  cvlatexch3  29821  cvlcvr1  29822  cvlcvrp  29823  cvlatcvr1  29824  cvlatcvr2  29825  cvlsupr2  29826  cvlsupr7  29831  cvlsupr8  29832  hlatjcl  29849  hlatjcom  29850  hlatjidm  29851  hlatjass  29852  hlatj32  29854  hlatj4  29856  hlatlej1  29857  atnlej1  29861  atnlej2  29862  hlrelat5N  29883  hlrelat  29884  hlrelat2  29885  exatleN  29886  cvr2N  29893  hlrelat3  29894  cvrval3  29895  cvrval5  29897  cvrexchlem  29901  cvratlem  29903  cvrat  29904  atcvr0eq  29908  lnnat  29909  cvrat2  29911  atcvrneN  29912  atcvrj1  29913  atcvrj2b  29914  atltcvr  29917  atle  29918  atlelt  29920  2atlt  29921  atexchcvrN  29922  cvrat3  29924  cvrat4  29925  cvrat42  29926  2atjm  29927  atbtwn  29928  3noncolr2  29931  4noncolr3  29935  athgt  29938  3dim0  29939  3dimlem3a  29942  3dimlem3OLDN  29944  3dimlem4a  29945  3dimlem4OLDN  29947  3dim3  29951  2dim  29952  1cvratex  29955  1cvrjat  29957  1cvrat  29958  ps-1  29959  ps-2  29960  hlatexch3N  29962  hlatexch4  29963  ps-2b  29964  3atlem1  29965  3atlem2  29966  3atlem4  29968  3atlem5  29969  3atlem6  29970  3at  29972  islln3  29992  llnnleat  29995  llnn0  29998  llnle  30000  llnexatN  30003  llncmp  30004  2llnmat  30006  2at0mat0  30007  2atm  30009  ps-2c  30010  lplni2  30019  lplnle  30022  lplnnle2at  30023  lplnn0N  30029  islpln2a  30030  2atmat  30043  lplnexllnN  30046  2llnjaN  30048  2llnm4  30052  2llnmeqat  30053  lvoli3  30059  islvol5  30061  lvoli2  30063  lvolnle3at  30064  3atnelvolN  30068  lvoln0N  30073  islvol2aN  30074  4atlem3  30078  4atlem3a  30079  4atlem3b  30080  4atlem4a  30081  4atlem4b  30082  4atlem4c  30083  4atlem4d  30084  4atlem9  30085  4atlem10a  30086  4atlem10  30088  4atlem11a  30089  4atlem11b  30090  4atlem11  30091  4atlem12a  30092  4atlem12b  30093  4atlem12  30094  4at2  30096  lplncvrlvol2  30097  2lplnja  30101  dalempeb  30121  dalemqeb  30122  dalemreb  30123  dalemseb  30124  dalemteb  30125  dalemueb  30126  dalem3  30146  dalem16  30161  dalemcceb  30171  dalem21  30176  dalem25  30180  dalem38  30192  dalem39  30193  dalem43  30197  dalem44  30198  dalem45  30199  dalem53  30207  dalem54  30208  dalem55  30209  dalem57  30211  dalem60  30214  snatpsubN  30232  linepsubN  30234  pmaple  30243  pmapat  30245  pmap1N  30249  pmapsub  30250  pmapglbx  30251  isline2  30256  linepmap  30257  isline3  30258  isline4N  30259  lneq2at  30260  lncvrelatN  30263  lncmp  30265  2lnat  30266  2atm2atN  30267  2llnma1b  30268  2llnma1  30269  2llnma3r  30270  cdlema1N  30273  cdlemblem  30275  cdlemb  30276  elpaddn0  30282  paddcom  30295  paddasslem2  30303  paddasslem5  30306  paddasslem12  30313  paddasslem13  30314  pmapjoin  30334  pmapjat1  30335  pmapjat2  30336  pmapjlln1  30337  atmod1i1  30339  atmod1i2  30341  llnmod1i2  30342  atmod2i1  30343  atmod2i2  30344  atmod3i1  30346  atmod3i2  30347  atmod4i1  30348  atmod4i2  30349  llnexchb2lem  30350  llnexchb2  30351  dalawlem2  30354  dalawlem3  30355  dalawlem5  30357  dalawlem6  30358  dalawlem7  30359  dalawlem8  30360  dalawlem11  30363  dalawlem12  30364  polval2N  30388  pol1N  30392  polatN  30413  2polatN  30414  paddatclN  30431  linepsubclN  30433  lhp2lt  30483  lhp0lt  30485  lhpexle2lem  30491  lhpexle3lem  30493  lhpjat2  30503  lhpj1  30504  lhpmcvr3  30507  lhpmcvr4N  30508  lhpmcvr5N  30509  lhpmcvr6N  30510  lhpmatb  30513  lhp2at0  30514  lhp2atnle  30515  lhp2at0nle  30517  lhprelat3N  30522  lhple  30524  lhpat4N  30526  lhpat3  30528  4atexlemtlw  30549  4atexlemc  30551  4atexlemnclw  30552  4atexlemcnd  30554  4atex2-0aOLDN  30560  lauteq  30577  ltrnid  30617  ltrnel  30621  ltrnat  30622  ltrncnvat  30623  ltrncnvel  30624  ltrncoval  30627  ltrncnv  30628  ltrn11at  30629  ltrneq2  30630  ltrneq  30631  idltrn  30632  ltrnmw  30633  trlval2  30645  trlcnv  30647  trljat1  30648  trljat2  30649  ltrnideq  30657  arglem1N  30672  cdlemc1  30673  cdlemc2  30674  cdlemc4  30676  cdlemc5  30677  cdlemc6  30678  cdlemd1  30680  cdlemd2  30681  cdlemd3  30682  cdlemd4  30683  cdlemd7  30686  cdleme0aa  30692  cdleme0b  30694  cdleme0c  30695  cdleme0cp  30696  cdleme0cq  30697  cdleme0e  30699  cdleme0fN  30700  cdleme1b  30708  cdleme1  30709  cdleme2  30710  cdleme3b  30711  cdleme3c  30712  cdleme3e  30714  cdleme3g  30716  cdleme3h  30717  cdleme3  30719  cdleme5  30722  cdleme7d  30728  cdleme7e  30729  cdleme7ga  30730  cdleme7  30731  cdleme8  30732  cdleme9  30735  cdleme10  30736  cdleme11c  30743  cdleme11e  30745  cdleme11fN  30746  cdleme11g  30747  cdleme11k  30750  cdleme11  30752  cdleme15b  30757  cdleme15  30760  cdleme16b  30761  cdleme17b  30769  cdleme17c  30770  cdlemednpq  30781  cdleme20zN  30783  cdleme20y  30784  cdleme19a  30785  cdleme20bN  30792  cdleme20d  30794  cdleme20j  30800  cdleme21c  30809  cdleme22aa  30821  cdleme22b  30823  cdleme22cN  30824  cdleme22d  30825  cdleme22e  30826  cdleme22eALTN  30827  cdleme23b  30832  cdleme23c  30833  cdleme27N  30851  cdleme28a  30852  cdleme30a  30860  cdlemefrs29pre00  30877  cdlemefrs29bpre0  30878  cdlemefrs29cpre1  30880  cdlemefrs32fva  30882  cdlemefrs32fva1  30883  cdlemefr32snb  30887  cdlemefs32snb  30897  cdleme32snb  30918  cdleme32fva  30919  cdleme32fva1  30920  cdleme32fvaw  30921  cdleme35a  30930  cdleme35fnpq  30931  cdleme35b  30932  cdleme35c  30933  cdleme35f  30936  cdleme42c  30954  cdleme42e  30961  cdleme42h  30964  cdleme42i  30965  cdleme42ke  30967  cdleme42keg  30968  cdleme42mgN  30970  cdleme17d4  30979  cdleme48fvg  30982  cdleme48bw  30984  cdlemeg46req  31011  cdleme50trn3  31035  cdlemf1  31043  cdlemf2  31044  trlord  31051  ltrniotacnvval  31064  cdlemg2fv2  31082  cdlemg2l  31085  cdlemg7fvbwN  31089  cdlemg4c  31094  cdlemg4  31099  cdlemg6c  31102  cdlemg8b  31110  cdlemg11b  31124  cdlemg13a  31133  cdlemg17a  31143  cdlemg17h  31150  cdlemg17  31159  cdlemg18b  31161  cdlemg19a  31165  cdlemg27a  31174  cdlemg27b  31178  cdlemg31a  31179  cdlemg31b  31180  cdlemg31d  31182  cdlemg33b0  31183  cdlemg33a  31188  cdlemg35  31195  trlcolem  31208  cdlemg42  31211  cdlemg44a  31213  cdlemg46  31217  cdlemh1  31297  cdlemh2  31298  cdlemh  31299  cdlemi1  31300  cdlemi  31302  cdlemk3  31315  cdlemk4  31316  cdlemkvcl  31324  cdlemk7  31330  cdlemk11  31331  cdlemk15  31337  cdlemk1u  31341  cdlemk7u  31352  cdlemk11u  31353  cdlemk37  31396  cdlemk39  31398  cdlemkid1  31404  cdlemkid2  31406  cdlemk48  31432  cdlemk50  31434  cdlemk51  31435  cdlemk52  31436  dia2dimlem1  31547  dia2dimlem2  31548  dia2dimlem3  31549  dia2dimlem5  31551  dia2dimlem7  31553  dia2dimlem9  31555  dia2dimlem10  31556  dia2dimlem12  31558  dia2dimlem13  31559  cdlemm10N  31601  cdlemn2  31678  cdlemn3  31680  cdlemn9  31688  cdlemn10  31689  dihjustlem  31699  dihord1  31701  dihord2pre2  31709  dihvalcqat  31722  dib2dim  31726  dih2dimb  31727  dih2dimbALTN  31728  dihord5apre  31745  dihglbcpreN  31783  dihmeetlem3N  31788  dihmeetlem6  31792  dihjatc1  31794  dihjatc2N  31795  dihjatc3  31796  dihmeetlem9N  31798  dihmeetlem10N  31799  dihmeetlem11N  31800  dihmeetlem13N  31802  dihmeetlem15N  31804  dihmeetlem16N  31805  dihmeetlem17N  31806  dihatexv2  31822  dihjatb  31899  dihjatc  31900  dihjatcclem1  31901  dihjatcclem2  31902  dihjatcclem4  31904  dihjat  31906  dihjat3  31915  dihjat5N  31920  dvh4dimat  31921
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 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363
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 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-iota 5377  df-fun 5415  df-fv 5421  df-ats 29750
  Copyright terms: Public domain W3C validator