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

Theorem atbase 30185
Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 23878 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 3618 . . . 4  |-  ( P  e.  A  ->  -.  A  =  (/) )
2 atombase.a . . . . 5  |-  A  =  ( Atoms `  K )
32eqeq1i 2449 . . . 4  |-  ( A  =  (/)  <->  ( Atoms `  K
)  =  (/) )
41, 3sylnib 297 . . 3  |-  ( P  e.  A  ->  -.  ( Atoms `  K )  =  (/) )
5 fvprc 5751 . . 3  |-  ( -.  K  e.  _V  ->  (
Atoms `  K )  =  (/) )
64, 5nsyl2 122 . 2  |-  ( P  e.  A  ->  K  e.  _V )
7 atombase.b . . . 4  |-  B  =  ( Base `  K
)
8 eqid 2442 . . . 4  |-  ( 0.
`  K )  =  ( 0. `  K
)
9 eqid 2442 . . . 4  |-  (  <o  `  K )  =  ( 
<o  `  K )
107, 8, 9, 2isat 30182 . . 3  |-  ( K  e.  _V  ->  ( P  e.  A  <->  ( P  e.  B  /\  ( 0. `  K ) ( 
<o  `  K ) P ) ) )
1110simprbda 608 . 2  |-  ( ( K  e.  _V  /\  P  e.  A )  ->  P  e.  B )
126, 11mpancom 652 1  |-  ( P  e.  A  ->  P  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1727   _Vcvv 2962   (/)c0 3613   class class class wbr 4237   ` cfv 5483   Basecbs 13500   0.cp0 14497    <o ccvr 30158   Atomscatm 30159
This theorem is referenced by:  atssbase  30186  0ltat  30187  leatb  30188  meetat  30192  atnle0  30205  atlen0  30206  atcmp  30207  atcvreq0  30210  atncvrN  30211  atnle  30213  atnem0  30214  atlatmstc  30215  atlatle  30216  cvlexch2  30225  cvlexchb1  30226  cvlexchb2  30227  cvlatexchb1  30230  cvlatexchb2  30231  cvlatexch1  30232  cvlatexch2  30233  cvlatexch3  30234  cvlcvr1  30235  cvlcvrp  30236  cvlatcvr1  30237  cvlatcvr2  30238  cvlsupr2  30239  cvlsupr7  30244  cvlsupr8  30245  hlatjcl  30262  hlatjcom  30263  hlatjidm  30264  hlatjass  30265  hlatj32  30267  hlatj4  30269  hlatlej1  30270  atnlej1  30274  atnlej2  30275  hlrelat5N  30296  hlrelat  30297  hlrelat2  30298  exatleN  30299  cvr2N  30306  hlrelat3  30307  cvrval3  30308  cvrval5  30310  cvrexchlem  30314  cvratlem  30316  cvrat  30317  atcvr0eq  30321  lnnat  30322  cvrat2  30324  atcvrneN  30325  atcvrj1  30326  atcvrj2b  30327  atltcvr  30330  atle  30331  atlelt  30333  2atlt  30334  atexchcvrN  30335  cvrat3  30337  cvrat4  30338  cvrat42  30339  2atjm  30340  atbtwn  30341  3noncolr2  30344  4noncolr3  30348  athgt  30351  3dim0  30352  3dimlem3a  30355  3dimlem3OLDN  30357  3dimlem4a  30358  3dimlem4OLDN  30360  3dim3  30364  2dim  30365  1cvratex  30368  1cvrjat  30370  1cvrat  30371  ps-1  30372  ps-2  30373  hlatexch3N  30375  hlatexch4  30376  ps-2b  30377  3atlem1  30378  3atlem2  30379  3atlem4  30381  3atlem5  30382  3atlem6  30383  3at  30385  islln3  30405  llnnleat  30408  llnn0  30411  llnle  30413  llnexatN  30416  llncmp  30417  2llnmat  30419  2at0mat0  30420  2atm  30422  ps-2c  30423  lplni2  30432  lplnle  30435  lplnnle2at  30436  lplnn0N  30442  islpln2a  30443  2atmat  30456  lplnexllnN  30459  2llnjaN  30461  2llnm4  30465  2llnmeqat  30466  lvoli3  30472  islvol5  30474  lvoli2  30476  lvolnle3at  30477  3atnelvolN  30481  lvoln0N  30486  islvol2aN  30487  4atlem3  30491  4atlem3a  30492  4atlem3b  30493  4atlem4a  30494  4atlem4b  30495  4atlem4c  30496  4atlem4d  30497  4atlem9  30498  4atlem10a  30499  4atlem10  30501  4atlem11a  30502  4atlem11b  30503  4atlem11  30504  4atlem12a  30505  4atlem12b  30506  4atlem12  30507  4at2  30509  lplncvrlvol2  30510  2lplnja  30514  dalempeb  30534  dalemqeb  30535  dalemreb  30536  dalemseb  30537  dalemteb  30538  dalemueb  30539  dalem3  30559  dalem16  30574  dalemcceb  30584  dalem21  30589  dalem25  30593  dalem38  30605  dalem39  30606  dalem43  30610  dalem44  30611  dalem45  30612  dalem53  30620  dalem54  30621  dalem55  30622  dalem57  30624  dalem60  30627  snatpsubN  30645  linepsubN  30647  pmaple  30656  pmapat  30658  pmap1N  30662  pmapsub  30663  pmapglbx  30664  isline2  30669  linepmap  30670  isline3  30671  isline4N  30672  lneq2at  30673  lncvrelatN  30676  lncmp  30678  2lnat  30679  2atm2atN  30680  2llnma1b  30681  2llnma1  30682  2llnma3r  30683  cdlema1N  30686  cdlemblem  30688  cdlemb  30689  elpaddn0  30695  paddcom  30708  paddasslem2  30716  paddasslem5  30719  paddasslem12  30726  paddasslem13  30727  pmapjoin  30747  pmapjat1  30748  pmapjat2  30749  pmapjlln1  30750  atmod1i1  30752  atmod1i2  30754  llnmod1i2  30755  atmod2i1  30756  atmod2i2  30757  atmod3i1  30759  atmod3i2  30760  atmod4i1  30761  atmod4i2  30762  llnexchb2lem  30763  llnexchb2  30764  dalawlem2  30767  dalawlem3  30768  dalawlem5  30770  dalawlem6  30771  dalawlem7  30772  dalawlem8  30773  dalawlem11  30776  dalawlem12  30777  polval2N  30801  pol1N  30805  polatN  30826  2polatN  30827  paddatclN  30844  linepsubclN  30846  lhp2lt  30896  lhp0lt  30898  lhpexle2lem  30904  lhpexle3lem  30906  lhpjat2  30916  lhpj1  30917  lhpmcvr3  30920  lhpmcvr4N  30921  lhpmcvr5N  30922  lhpmcvr6N  30923  lhpmatb  30926  lhp2at0  30927  lhp2atnle  30928  lhp2at0nle  30930  lhprelat3N  30935  lhple  30937  lhpat4N  30939  lhpat3  30941  4atexlemtlw  30962  4atexlemc  30964  4atexlemnclw  30965  4atexlemcnd  30967  4atex2-0aOLDN  30973  lauteq  30990  ltrnid  31030  ltrnel  31034  ltrnat  31035  ltrncnvat  31036  ltrncnvel  31037  ltrncoval  31040  ltrncnv  31041  ltrn11at  31042  ltrneq2  31043  ltrneq  31044  idltrn  31045  ltrnmw  31046  trlval2  31058  trlcnv  31060  trljat1  31061  trljat2  31062  ltrnideq  31070  arglem1N  31085  cdlemc1  31086  cdlemc2  31087  cdlemc4  31089  cdlemc5  31090  cdlemc6  31091  cdlemd1  31093  cdlemd2  31094  cdlemd3  31095  cdlemd4  31096  cdlemd7  31099  cdleme0aa  31105  cdleme0b  31107  cdleme0c  31108  cdleme0cp  31109  cdleme0cq  31110  cdleme0e  31112  cdleme0fN  31113  cdleme1b  31121  cdleme1  31122  cdleme2  31123  cdleme3b  31124  cdleme3c  31125  cdleme3e  31127  cdleme3g  31129  cdleme3h  31130  cdleme3  31132  cdleme5  31135  cdleme7d  31141  cdleme7e  31142  cdleme7ga  31143  cdleme7  31144  cdleme8  31145  cdleme9  31148  cdleme10  31149  cdleme11c  31156  cdleme11e  31158  cdleme11fN  31159  cdleme11g  31160  cdleme11k  31163  cdleme11  31165  cdleme15b  31170  cdleme15  31173  cdleme16b  31174  cdleme17b  31182  cdleme17c  31183  cdlemednpq  31194  cdleme20zN  31196  cdleme20y  31197  cdleme19a  31198  cdleme20bN  31205  cdleme20d  31207  cdleme20j  31213  cdleme21c  31222  cdleme22aa  31234  cdleme22b  31236  cdleme22cN  31237  cdleme22d  31238  cdleme22e  31239  cdleme22eALTN  31240  cdleme23b  31245  cdleme23c  31246  cdleme27N  31264  cdleme28a  31265  cdleme30a  31273  cdlemefrs29pre00  31290  cdlemefrs29bpre0  31291  cdlemefrs29cpre1  31293  cdlemefrs32fva  31295  cdlemefrs32fva1  31296  cdlemefr32snb  31300  cdlemefs32snb  31310  cdleme32snb  31331  cdleme32fva  31332  cdleme32fva1  31333  cdleme32fvaw  31334  cdleme35a  31343  cdleme35fnpq  31344  cdleme35b  31345  cdleme35c  31346  cdleme35f  31349  cdleme42c  31367  cdleme42e  31374  cdleme42h  31377  cdleme42i  31378  cdleme42ke  31380  cdleme42keg  31381  cdleme42mgN  31383  cdleme17d4  31392  cdleme48fvg  31395  cdleme48bw  31397  cdlemeg46req  31424  cdleme50trn3  31448  cdlemf1  31456  cdlemf2  31457  trlord  31464  ltrniotacnvval  31477  cdlemg2fv2  31495  cdlemg2l  31498  cdlemg7fvbwN  31502  cdlemg4c  31507  cdlemg4  31512  cdlemg6c  31515  cdlemg8b  31523  cdlemg11b  31537  cdlemg13a  31546  cdlemg17a  31556  cdlemg17h  31563  cdlemg17  31572  cdlemg18b  31574  cdlemg19a  31578  cdlemg27a  31587  cdlemg27b  31591  cdlemg31a  31592  cdlemg31b  31593  cdlemg31d  31595  cdlemg33b0  31596  cdlemg33a  31601  cdlemg35  31608  trlcolem  31621  cdlemg42  31624  cdlemg44a  31626  cdlemg46  31630  cdlemh1  31710  cdlemh2  31711  cdlemh  31712  cdlemi1  31713  cdlemi  31715  cdlemk3  31728  cdlemk4  31729  cdlemkvcl  31737  cdlemk7  31743  cdlemk11  31744  cdlemk15  31750  cdlemk1u  31754  cdlemk7u  31765  cdlemk11u  31766  cdlemk37  31809  cdlemk39  31811  cdlemkid1  31817  cdlemkid2  31819  cdlemk48  31845  cdlemk50  31847  cdlemk51  31848  cdlemk52  31849  dia2dimlem1  31960  dia2dimlem2  31961  dia2dimlem3  31962  dia2dimlem5  31964  dia2dimlem7  31966  dia2dimlem9  31968  dia2dimlem10  31969  dia2dimlem12  31971  dia2dimlem13  31972  cdlemm10N  32014  cdlemn2  32091  cdlemn3  32093  cdlemn9  32101  cdlemn10  32102  dihjustlem  32112  dihord1  32114  dihord2pre2  32122  dihvalcqat  32135  dib2dim  32139  dih2dimb  32140  dih2dimbALTN  32141  dihord5apre  32158  dihglbcpreN  32196  dihmeetlem3N  32201  dihmeetlem6  32205  dihjatc1  32207  dihjatc2N  32208  dihjatc3  32209  dihmeetlem9N  32211  dihmeetlem10N  32212  dihmeetlem11N  32213  dihmeetlem13N  32215  dihmeetlem15N  32217  dihmeetlem16N  32218  dihmeetlem17N  32219  dihatexv2  32235  dihjatb  32312  dihjatc  32313  dihjatcclem1  32314  dihjatcclem2  32315  dihjatcclem4  32317  dihjat  32319  dihjat3  32328  dihjat5N  32333  dvh4dimat  32334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-13 1729  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-sep 4355  ax-nul 4363  ax-pow 4406  ax-pr 4432
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-mo 2292  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2716  df-rex 2717  df-rab 2720  df-v 2964  df-sbc 3168  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-nul 3614  df-if 3764  df-sn 3844  df-pr 3845  df-op 3847  df-uni 4040  df-br 4238  df-opab 4292  df-mpt 4293  df-id 4527  df-xp 4913  df-rel 4914  df-cnv 4915  df-co 4916  df-dm 4917  df-iota 5447  df-fun 5485  df-fv 5491  df-ats 30163
  Copyright terms: Public domain W3C validator