Theorem atbase 34576

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 29203 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

Step	Hyp	Ref	Expression
1		n0i 3920	. . . 4 |- ( P e. A -> -. A = (/) )
2		atombase.a	. . . . 5 |- A = ( Atoms ` K )
3	2	eqeq1i 2627	. . . 4 |- ( A = (/) <-> ( Atoms ` K ) = (/) )
4	1, 3	sylnib 318	. . 3 |- ( P e. A -> -. ( Atoms ` K ) = (/) )
5		fvprc 6185	. . 3 |- ( -. K e. _V -> ( Atoms ` K ) = (/) )
6	4, 5	nsyl2 142	. 2 |- ( P e. A -> K e. _V )
7		atombase.b	. . . 4 |- B = ( Base ` K )
8		eqid 2622	. . . 4 |- ( 0. ` K ) = ( 0. ` K )
9		eqid 2622	. . . 4 |- ( <o ` K ) = ( <o ` K )
10	7, 8, 9, 2	isat 34573	. . 3 |- ( K e. _V -> ( P e. A <-> ( P e. B /\ ( 0. ` K ) ( <o ` K ) P ) ) )
11	10	simprbda 653	. 2 |- ( ( K e. _V /\ P e. A ) -> P e. B )
12	6, 11	mpancom 703	1 |- ( P e. A -> P e. B )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   _Vcvv 3200   (/)c0 3915   class class class wbr 4653   ` cfv 5888   Basecbs 15857   0.cp0 17037   <o ccvr 34549   Atomscatm 34550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896  df-ats 34554

This theorem is referenced by:  atssbase  34577  0ltat  34578  leatb  34579  meetat  34583  atnle0  34596  atlen0  34597  atcmp  34598  atcvreq0  34601  atncvrN  34602  atnle  34604  atnem0  34605  atlatmstc  34606  atlatle  34607  cvlexch2  34616  cvlexchb1  34617  cvlexchb2  34618  cvlatexchb1  34621  cvlatexchb2  34622  cvlatexch1  34623  cvlatexch2  34624  cvlatexch3  34625  cvlcvr1  34626  cvlcvrp  34627  cvlatcvr1  34628  cvlatcvr2  34629  cvlsupr2  34630  cvlsupr7  34635  cvlsupr8  34636  hlatjcl  34653  hlatjcom  34654  hlatjidm  34655  hlatjass  34656  hlatj32  34658  hlatj4  34660  hlatlej1  34661  atnlej1  34665  atnlej2  34666  hlrelat5N  34687  hlrelat  34688  hlrelat2  34689  exatleN  34690  cvr2N  34697  hlrelat3  34698  cvrval3  34699  cvrval5  34701  cvrexchlem  34705  cvratlem  34707  cvrat  34708  atcvr0eq  34712  lnnat  34713  cvrat2  34715  atcvrneN  34716  atcvrj1  34717  atcvrj2b  34718  atltcvr  34721  atle  34722  atlelt  34724  2atlt  34725  atexchcvrN  34726  cvrat3  34728  cvrat4  34729  cvrat42  34730  2atjm  34731  atbtwn  34732  3noncolr2  34735  4noncolr3  34739  athgt  34742  3dim0  34743  3dimlem3a  34746  3dimlem3OLDN  34748  3dimlem4a  34749  3dimlem4OLDN  34751  3dim3  34755  2dim  34756  1cvratex  34759  1cvrjat  34761  1cvrat  34762  ps-1  34763  ps-2  34764  hlatexch3N  34766  hlatexch4  34767  ps-2b  34768  3atlem1  34769  3atlem2  34770  3atlem4  34772  3atlem5  34773  3atlem6  34774  3at  34776  islln3  34796  llnnleat  34799  llnn0  34802  llnle  34804  llnexatN  34807  llncmp  34808  2llnmat  34810  2at0mat0  34811  2atm  34813  ps-2c  34814  lplni2  34823  lplnle  34826  lplnnle2at  34827  lplnn0N  34833  islpln2a  34834  2atmat  34847  lplnexllnN  34850  2llnjaN  34852  2llnm4  34856  2llnmeqat  34857  lvoli3  34863  islvol5  34865  lvoli2  34867  lvolnle3at  34868  3atnelvolN  34872  lvoln0N  34877  islvol2aN  34878  4atlem3  34882  4atlem3a  34883  4atlem3b  34884  4atlem4a  34885  4atlem4b  34886  4atlem4c  34887  4atlem4d  34888  4atlem9  34889  4atlem10a  34890  4atlem10  34892  4atlem11a  34893  4atlem11b  34894  4atlem11  34895  4atlem12a  34896  4atlem12b  34897  4atlem12  34898  4at2  34900  lplncvrlvol2  34901  2lplnja  34905  dalempeb  34925  dalemqeb  34926  dalemreb  34927  dalemseb  34928  dalemteb  34929  dalemueb  34930  dalem3  34950  dalem16  34965  dalemcceb  34975  dalem21  34980  dalem25  34984  dalem38  34996  dalem39  34997  dalem43  35001  dalem44  35002  dalem45  35003  dalem53  35011  dalem54  35012  dalem55  35013  dalem57  35015  dalem60  35018  snatpsubN  35036  linepsubN  35038  pmaple  35047  pmapat  35049  pmap1N  35053  pmapsub  35054  pmapglbx  35055  isline2  35060  linepmap  35061  isline3  35062  isline4N  35063  lneq2at  35064  lncvrelatN  35067  lncmp  35069  2lnat  35070  2atm2atN  35071  2llnma1b  35072  2llnma1  35073  2llnma3r  35074  cdlema1N  35077  cdlemblem  35079  cdlemb  35080  elpaddn0  35086  paddcom  35099  paddasslem2  35107  paddasslem5  35110  paddasslem12  35117  paddasslem13  35118  pmapjoin  35138  pmapjat1  35139  pmapjat2  35140  pmapjlln1  35141  atmod1i1  35143  atmod1i2  35145  llnmod1i2  35146  atmod2i1  35147  atmod2i2  35148  atmod3i1  35150  atmod3i2  35151  atmod4i1  35152  atmod4i2  35153  llnexchb2lem  35154  llnexchb2  35155  dalawlem2  35158  dalawlem3  35159  dalawlem5  35161  dalawlem6  35162  dalawlem7  35163  dalawlem8  35164  dalawlem11  35167  dalawlem12  35168  polval2N  35192  pol1N  35196  polatN  35217  2polatN  35218  paddatclN  35235  linepsubclN  35237  lhp2lt  35287  lhp0lt  35289  lhpexle2lem  35295  lhpexle3lem  35297  lhpjat2  35307  lhpj1  35308  lhpmcvr3  35311  lhpmcvr4N  35312  lhpmcvr5N  35313  lhpmcvr6N  35314  lhpmatb  35317  lhp2at0  35318  lhp2atnle  35319  lhp2at0nle  35321  lhprelat3N  35326  lhple  35328  lhpat4N  35330  lhpat3  35332  4atexlemtlw  35353  4atexlemc  35355  4atexlemnclw  35356  4atexlemcnd  35358  4atex2-0aOLDN  35364  lauteq  35381  ltrnid  35421  ltrnel  35425  ltrnat  35426  ltrncnvat  35427  ltrncnvel  35428  ltrncoval  35431  ltrncnv  35432  ltrn11at  35433  ltrneq2  35434  ltrneq  35435  idltrn  35436  ltrnmwOLD  35438  trlval2  35450  trlcnv  35452  trljat1  35453  trljat2  35454  ltrnideq  35462  arglem1N  35477  cdlemc1  35478  cdlemc2  35479  cdlemc4  35481  cdlemc5  35482  cdlemc6  35483  cdlemd1  35485  cdlemd2  35486  cdlemd3  35487  cdlemd4  35488  cdlemd7  35491  cdleme0aa  35497  cdleme0b  35499  cdleme0c  35500  cdleme0cp  35501  cdleme0cq  35502  cdleme0e  35504  cdleme0fN  35505  cdleme1b  35513  cdleme1  35514  cdleme2  35515  cdleme3b  35516  cdleme3c  35517  cdleme3e  35519  cdleme3g  35521  cdleme3h  35522  cdleme3  35524  cdleme5  35527  cdleme7d  35533  cdleme7e  35534  cdleme7ga  35535  cdleme7  35536  cdleme8  35537  cdleme9  35540  cdleme10  35541  cdleme11c  35548  cdleme11e  35550  cdleme11fN  35551  cdleme11g  35552  cdleme11k  35555  cdleme11  35557  cdleme15b  35562  cdleme15  35565  cdleme16b  35566  cdleme17b  35574  cdleme17c  35575  cdlemednpq  35586  cdleme20zN  35588  cdleme20yOLD  35590  cdleme19a  35591  cdleme20bN  35598  cdleme20d  35600  cdleme20j  35606  cdleme21c  35615  cdleme22aa  35627  cdleme22b  35629  cdleme22cN  35630  cdleme22d  35631  cdleme22e  35632  cdleme22eALTN  35633  cdleme23b  35638  cdleme23c  35639  cdleme27N  35657  cdleme28a  35658  cdleme30a  35666  cdlemefrs29pre00  35683  cdlemefrs29bpre0  35684  cdlemefrs29cpre1  35686  cdlemefrs32fva  35688  cdlemefrs32fva1  35689  cdlemefr32snb  35693  cdlemefs32snb  35703  cdleme32snb  35724  cdleme32fva  35725  cdleme32fva1  35726  cdleme32fvaw  35727  cdleme35a  35736  cdleme35fnpq  35737  cdleme35b  35738  cdleme35c  35739  cdleme35f  35742  cdleme42c  35760  cdleme42e  35767  cdleme42h  35770  cdleme42i  35771  cdleme42ke  35773  cdleme42keg  35774  cdleme42mgN  35776  cdleme17d4  35785  cdleme48fvg  35788  cdleme48bw  35790  cdlemeg46req  35817  cdleme50trn3  35841  cdlemf1  35849  cdlemf2  35850  trlord  35857  ltrniotacnvval  35870  cdlemg2fv2  35888  cdlemg2l  35891  cdlemg7fvbwN  35895  cdlemg4c  35900  cdlemg4  35905  cdlemg6c  35908  cdlemg8b  35916  cdlemg11b  35930  cdlemg13a  35939  cdlemg17a  35949  cdlemg17h  35956  cdlemg17  35965  cdlemg18b  35967  cdlemg19a  35971  cdlemg27a  35980  cdlemg27b  35984  cdlemg31a  35985  cdlemg31b  35986  cdlemg31d  35988  cdlemg33b0  35989  cdlemg33a  35994  cdlemg35  36001  trlcolem  36014  cdlemg42  36017  cdlemg44a  36019  cdlemg46  36023  cdlemh1  36103  cdlemh2  36104  cdlemh  36105  cdlemi1  36106  cdlemi  36108  cdlemk3  36121  cdlemk4  36122  cdlemkvcl  36130  cdlemk7  36136  cdlemk11  36137  cdlemk15  36143  cdlemk1u  36147  cdlemk7u  36158  cdlemk11u  36159  cdlemk37  36202  cdlemk39  36204  cdlemkid1  36210  cdlemkid2  36212  cdlemk48  36238  cdlemk50  36240  cdlemk51  36241  cdlemk52  36242  dia2dimlem1  36353  dia2dimlem2  36354  dia2dimlem3  36355  dia2dimlem5  36357  dia2dimlem7  36359  dia2dimlem9  36361  dia2dimlem10  36362  dia2dimlem12  36364  dia2dimlem13  36365  cdlemm10N  36407  cdlemn2  36484  cdlemn3  36486  cdlemn9  36494  cdlemn10  36495  dihjustlem  36505  dihord1  36507  dihord2pre2  36515  dihvalcqat  36528  dib2dim  36532  dih2dimb  36533  dih2dimbALTN  36534  dihord5apre  36551  dihglbcpreN  36589  dihmeetlem3N  36594  dihmeetlem6  36598  dihjatc1  36600  dihjatc2N  36601  dihjatc3  36602  dihmeetlem9N  36604  dihmeetlem10N  36605  dihmeetlem11N  36606  dihmeetlem13N  36608  dihmeetlem15N  36610  dihmeetlem16N  36611  dihmeetlem17N  36612  dihatexv2  36628  dihjatb  36705  dihjatc  36706  dihjatcclem1  36707  dihjatcclem2  36708  dihjatcclem4  36710  dihjat  36712  dihjat3  36721  dihjat5N  36726  dvh4dimat  36727