Theorem atbase 36419

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 30115 analog.) (Contributed by NM, 10-Oct-2011.)

Hypotheses

Ref	Expression
atombase.b	⊢ 𝐵 = (Base‘𝐾)
atombase.a	⊢ 𝐴 = (Atoms‘𝐾)

Assertion

Ref	Expression
atbase	⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

Proof of Theorem atbase

Step	Hyp	Ref	Expression
1		n0i 4298	. . . 4 ⊢ (𝑃 ∈ 𝐴 → ¬ 𝐴 = ∅)
2		atombase.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
3	2	eqeq1i 2826	. . . 4 ⊢ (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
4	1, 3	sylnib 330	. . 3 ⊢ (𝑃 ∈ 𝐴 → ¬ (Atoms‘𝐾) = ∅)
5		fvprc 6657	. . 3 ⊢ (¬ 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
6	4, 5	nsyl2 143	. 2 ⊢ (𝑃 ∈ 𝐴 → 𝐾 ∈ V)
7		atombase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2821	. . . 4 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		eqid 2821	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	isat 36416	. . 3 ⊢ (𝐾 ∈ V → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
11	10	simprbda 501	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐵)
12	6, 11	mpancom 686	1 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2110  Vcvv 3494  ∅c0 4290   class class class wbr 5058  ‘cfv 6349  Basecbs 16477  0.cp0 17641   ⋖ ccvr 36392  Atomscatm 36393

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-iota 6308  df-fun 6351  df-fv 6357  df-ats 36397

This theorem is referenced by:  atssbase  36420  0ltat  36421  leatb  36422  meetat  36426  atnle0  36439  atlen0  36440  atcmp  36441  atcvreq0  36444  atncvrN  36445  atnle  36447  atnem0  36448  atlatmstc  36449  atlatle  36450  cvlexch2  36459  cvlexchb1  36460  cvlexchb2  36461  cvlatexchb1  36464  cvlatexchb2  36465  cvlatexch1  36466  cvlatexch2  36467  cvlatexch3  36468  cvlcvr1  36469  cvlcvrp  36470  cvlatcvr1  36471  cvlatcvr2  36472  cvlsupr2  36473  cvlsupr7  36478  cvlsupr8  36479  hlatjcl  36497  hlatjcom  36498  hlatjidm  36499  hlatjass  36500  hlatj32  36502  hlatj4  36504  hlatlej1  36505  atnlej1  36509  atnlej2  36510  hlrelat5N  36531  hlrelat  36532  hlrelat2  36533  exatleN  36534  cvr2N  36541  hlrelat3  36542  cvrval3  36543  cvrval5  36545  cvrexchlem  36549  cvratlem  36551  cvrat  36552  atcvr0eq  36556  lnnat  36557  cvrat2  36559  atcvrneN  36560  atcvrj1  36561  atcvrj2b  36562  atltcvr  36565  atle  36566  atlelt  36568  2atlt  36569  atexchcvrN  36570  cvrat3  36572  cvrat4  36573  cvrat42  36574  2atjm  36575  atbtwn  36576  3noncolr2  36579  4noncolr3  36583  athgt  36586  3dim0  36587  3dimlem3a  36590  3dimlem3OLDN  36592  3dimlem4a  36593  3dimlem4OLDN  36595  3dim3  36599  2dim  36600  1cvratex  36603  1cvrjat  36605  1cvrat  36606  ps-1  36607  ps-2  36608  hlatexch3N  36610  hlatexch4  36611  ps-2b  36612  3atlem1  36613  3atlem2  36614  3atlem4  36616  3atlem5  36617  3atlem6  36618  3at  36620  islln3  36640  llnnleat  36643  llnn0  36646  llnle  36648  llnexatN  36651  llncmp  36652  2llnmat  36654  2at0mat0  36655  2atm  36657  ps-2c  36658  lplni2  36667  lplnle  36670  lplnnle2at  36671  lplnn0N  36677  islpln2a  36678  2atmat  36691  lplnexllnN  36694  2llnjaN  36696  2llnm4  36700  2llnmeqat  36701  lvoli3  36707  islvol5  36709  lvoli2  36711  lvolnle3at  36712  3atnelvolN  36716  lvoln0N  36721  islvol2aN  36722  4atlem3  36726  4atlem3a  36727  4atlem3b  36728  4atlem4a  36729  4atlem4b  36730  4atlem4c  36731  4atlem4d  36732  4atlem9  36733  4atlem10a  36734  4atlem10  36736  4atlem11a  36737  4atlem11b  36738  4atlem11  36739  4atlem12a  36740  4atlem12b  36741  4atlem12  36742  4at2  36744  lplncvrlvol2  36745  2lplnja  36749  dalempeb  36769  dalemqeb  36770  dalemreb  36771  dalemseb  36772  dalemteb  36773  dalemueb  36774  dalem3  36794  dalem16  36809  dalemcceb  36819  dalem21  36824  dalem25  36828  dalem38  36840  dalem39  36841  dalem43  36845  dalem44  36846  dalem45  36847  dalem53  36855  dalem54  36856  dalem55  36857  dalem57  36859  dalem60  36862  snatpsubN  36880  linepsubN  36882  pmaple  36891  pmapat  36893  pmap1N  36897  pmapsub  36898  pmapglbx  36899  isline2  36904  linepmap  36905  isline3  36906  isline4N  36907  lneq2at  36908  lncvrelatN  36911  lncmp  36913  2lnat  36914  2atm2atN  36915  2llnma1b  36916  2llnma1  36917  2llnma3r  36918  cdlema1N  36921  cdlemblem  36923  cdlemb  36924  elpaddn0  36930  paddcom  36943  paddasslem2  36951  paddasslem5  36954  paddasslem12  36961  paddasslem13  36962  pmapjoin  36982  pmapjat1  36983  pmapjat2  36984  pmapjlln1  36985  atmod1i1  36987  atmod1i2  36989  llnmod1i2  36990  atmod2i1  36991  atmod2i2  36992  atmod3i1  36994  atmod3i2  36995  atmod4i1  36996  atmod4i2  36997  llnexchb2lem  36998  llnexchb2  36999  dalawlem2  37002  dalawlem3  37003  dalawlem5  37005  dalawlem6  37006  dalawlem7  37007  dalawlem8  37008  dalawlem11  37011  dalawlem12  37012  polval2N  37036  pol1N  37040  polatN  37061  2polatN  37062  paddatclN  37079  linepsubclN  37081  lhp2lt  37131  lhp0lt  37133  lhpexle2lem  37139  lhpexle3lem  37141  lhpjat2  37151  lhpj1  37152  lhpmcvr3  37155  lhpmcvr4N  37156  lhpmcvr5N  37157  lhpmcvr6N  37158  lhpmatb  37161  lhp2at0  37162  lhp2atnle  37163  lhp2at0nle  37165  lhprelat3N  37170  lhple  37172  lhpat4N  37174  lhpat3  37176  4atexlemtlw  37197  4atexlemc  37199  4atexlemnclw  37200  4atexlemcnd  37202  4atex2-0aOLDN  37208  lauteq  37225  ltrnid  37265  ltrnel  37269  ltrnat  37270  ltrncnvat  37271  ltrncnvel  37272  ltrncoval  37275  ltrncnv  37276  ltrn11at  37277  ltrneq2  37278  ltrneq  37279  idltrn  37280  trlval2  37293  trlcnv  37295  trljat1  37296  trljat2  37297  ltrnideq  37305  arglem1N  37320  cdlemc1  37321  cdlemc2  37322  cdlemc4  37324  cdlemc5  37325  cdlemc6  37326  cdlemd1  37328  cdlemd2  37329  cdlemd3  37330  cdlemd4  37331  cdlemd7  37334  cdleme0aa  37340  cdleme0b  37342  cdleme0c  37343  cdleme0cp  37344  cdleme0cq  37345  cdleme0e  37347  cdleme0fN  37348  cdleme1b  37356  cdleme1  37357  cdleme2  37358  cdleme3b  37359  cdleme3c  37360  cdleme3e  37362  cdleme3g  37364  cdleme3h  37365  cdleme3  37367  cdleme5  37370  cdleme7d  37376  cdleme7e  37377  cdleme7ga  37378  cdleme7  37379  cdleme8  37380  cdleme9  37383  cdleme10  37384  cdleme11c  37391  cdleme11e  37393  cdleme11fN  37394  cdleme11g  37395  cdleme11k  37398  cdleme11  37400  cdleme15b  37405  cdleme15  37408  cdleme16b  37409  cdleme17b  37417  cdleme17c  37418  cdlemednpq  37429  cdleme20zN  37431  cdleme19a  37433  cdleme20bN  37440  cdleme20d  37442  cdleme20j  37448  cdleme21c  37457  cdleme22aa  37469  cdleme22b  37471  cdleme22cN  37472  cdleme22d  37473  cdleme22e  37474  cdleme22eALTN  37475  cdleme23b  37480  cdleme23c  37481  cdleme27N  37499  cdleme28a  37500  cdleme30a  37508  cdlemefrs29pre00  37525  cdlemefrs29bpre0  37526  cdlemefrs29cpre1  37528  cdlemefrs32fva  37530  cdlemefrs32fva1  37531  cdlemefr32snb  37535  cdlemefs32snb  37545  cdleme32snb  37566  cdleme32fva  37567  cdleme32fva1  37568  cdleme32fvaw  37569  cdleme35a  37578  cdleme35fnpq  37579  cdleme35b  37580  cdleme35c  37581  cdleme35f  37584  cdleme42c  37602  cdleme42e  37609  cdleme42h  37612  cdleme42i  37613  cdleme42ke  37615  cdleme42keg  37616  cdleme42mgN  37618  cdleme17d4  37627  cdleme48fvg  37630  cdleme48bw  37632  cdlemeg46req  37659  cdleme50trn3  37683  cdlemf1  37691  cdlemf2  37692  trlord  37699  ltrniotacnvval  37712  cdlemg2fv2  37730  cdlemg2l  37733  cdlemg7fvbwN  37737  cdlemg4c  37742  cdlemg4  37747  cdlemg6c  37750  cdlemg8b  37758  cdlemg11b  37772  cdlemg13a  37781  cdlemg17a  37791  cdlemg17h  37798  cdlemg17  37807  cdlemg18b  37809  cdlemg19a  37813  cdlemg27a  37822  cdlemg27b  37826  cdlemg31a  37827  cdlemg31b  37828  cdlemg31d  37830  cdlemg33b0  37831  cdlemg33a  37836  cdlemg35  37843  trlcolem  37856  cdlemg42  37859  cdlemg44a  37861  cdlemg46  37865  cdlemh1  37945  cdlemh2  37946  cdlemh  37947  cdlemi1  37948  cdlemi  37950  cdlemk3  37963  cdlemk4  37964  cdlemkvcl  37972  cdlemk7  37978  cdlemk11  37979  cdlemk15  37985  cdlemk1u  37989  cdlemk7u  38000  cdlemk11u  38001  cdlemk37  38044  cdlemk39  38046  cdlemkid1  38052  cdlemkid2  38054  cdlemk48  38080  cdlemk50  38082  cdlemk51  38083  cdlemk52  38084  dia2dimlem1  38194  dia2dimlem2  38195  dia2dimlem3  38196  dia2dimlem5  38198  dia2dimlem7  38200  dia2dimlem9  38202  dia2dimlem10  38203  dia2dimlem12  38205  dia2dimlem13  38206  cdlemm10N  38248  cdlemn2  38325  cdlemn3  38327  cdlemn9  38335  cdlemn10  38336  dihjustlem  38346  dihord1  38348  dihord2pre2  38356  dihvalcqat  38369  dib2dim  38373  dih2dimb  38374  dih2dimbALTN  38375  dihord5apre  38392  dihglbcpreN  38430  dihmeetlem3N  38435  dihmeetlem6  38439  dihjatc1  38441  dihjatc2N  38442  dihjatc3  38443  dihmeetlem9N  38445  dihmeetlem10N  38446  dihmeetlem11N  38447  dihmeetlem13N  38449  dihmeetlem15N  38451  dihmeetlem16N  38452  dihmeetlem17N  38453  dihatexv2  38469  dihjatb  38546  dihjatc  38547  dihjatcclem1  38548  dihjatcclem2  38549  dihjatcclem4  38551  dihjat  38553  dihjat3  38562  dihjat5N  38567  dvh4dimat  38568