Theorem atbase 33594

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 28587 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 3879	. . . 4 ⊢ (𝑃 ∈ 𝐴 → ¬ 𝐴 = ∅)
2		atombase.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
3	2	eqeq1i 2615	. . . 4 ⊢ (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
4	1, 3	sylnib 317	. . 3 ⊢ (𝑃 ∈ 𝐴 → ¬ (Atoms‘𝐾) = ∅)
5		fvprc 6097	. . 3 ⊢ (¬ 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
6	4, 5	nsyl2 141	. 2 ⊢ (𝑃 ∈ 𝐴 → 𝐾 ∈ V)
7		atombase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2610	. . . 4 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		eqid 2610	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	isat 33591	. . 3 ⊢ (𝐾 ∈ V → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
11	10	simprbda 651	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐵)
12	6, 11	mpancom 700	1 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  Vcvv 3173  ∅c0 3874   class class class wbr 4583  ‘cfv 5804  Basecbs 15695  0.cp0 16860   ⋖ ccvr 33567  Atomscatm 33568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-iota 5768  df-fun 5806  df-fv 5812  df-ats 33572

This theorem is referenced by:  atssbase  33595  0ltat  33596  leatb  33597  meetat  33601  atnle0  33614  atlen0  33615  atcmp  33616  atcvreq0  33619  atncvrN  33620  atnle  33622  atnem0  33623  atlatmstc  33624  atlatle  33625  cvlexch2  33634  cvlexchb1  33635  cvlexchb2  33636  cvlatexchb1  33639  cvlatexchb2  33640  cvlatexch1  33641  cvlatexch2  33642  cvlatexch3  33643  cvlcvr1  33644  cvlcvrp  33645  cvlatcvr1  33646  cvlatcvr2  33647  cvlsupr2  33648  cvlsupr7  33653  cvlsupr8  33654  hlatjcl  33671  hlatjcom  33672  hlatjidm  33673  hlatjass  33674  hlatj32  33676  hlatj4  33678  hlatlej1  33679  atnlej1  33683  atnlej2  33684  hlrelat5N  33705  hlrelat  33706  hlrelat2  33707  exatleN  33708  cvr2N  33715  hlrelat3  33716  cvrval3  33717  cvrval5  33719  cvrexchlem  33723  cvratlem  33725  cvrat  33726  atcvr0eq  33730  lnnat  33731  cvrat2  33733  atcvrneN  33734  atcvrj1  33735  atcvrj2b  33736  atltcvr  33739  atle  33740  atlelt  33742  2atlt  33743  atexchcvrN  33744  cvrat3  33746  cvrat4  33747  cvrat42  33748  2atjm  33749  atbtwn  33750  3noncolr2  33753  4noncolr3  33757  athgt  33760  3dim0  33761  3dimlem3a  33764  3dimlem3OLDN  33766  3dimlem4a  33767  3dimlem4OLDN  33769  3dim3  33773  2dim  33774  1cvratex  33777  1cvrjat  33779  1cvrat  33780  ps-1  33781  ps-2  33782  hlatexch3N  33784  hlatexch4  33785  ps-2b  33786  3atlem1  33787  3atlem2  33788  3atlem4  33790  3atlem5  33791  3atlem6  33792  3at  33794  islln3  33814  llnnleat  33817  llnn0  33820  llnle  33822  llnexatN  33825  llncmp  33826  2llnmat  33828  2at0mat0  33829  2atm  33831  ps-2c  33832  lplni2  33841  lplnle  33844  lplnnle2at  33845  lplnn0N  33851  islpln2a  33852  2atmat  33865  lplnexllnN  33868  2llnjaN  33870  2llnm4  33874  2llnmeqat  33875  lvoli3  33881  islvol5  33883  lvoli2  33885  lvolnle3at  33886  3atnelvolN  33890  lvoln0N  33895  islvol2aN  33896  4atlem3  33900  4atlem3a  33901  4atlem3b  33902  4atlem4a  33903  4atlem4b  33904  4atlem4c  33905  4atlem4d  33906  4atlem9  33907  4atlem10a  33908  4atlem10  33910  4atlem11a  33911  4atlem11b  33912  4atlem11  33913  4atlem12a  33914  4atlem12b  33915  4atlem12  33916  4at2  33918  lplncvrlvol2  33919  2lplnja  33923  dalempeb  33943  dalemqeb  33944  dalemreb  33945  dalemseb  33946  dalemteb  33947  dalemueb  33948  dalem3  33968  dalem16  33983  dalemcceb  33993  dalem21  33998  dalem25  34002  dalem38  34014  dalem39  34015  dalem43  34019  dalem44  34020  dalem45  34021  dalem53  34029  dalem54  34030  dalem55  34031  dalem57  34033  dalem60  34036  snatpsubN  34054  linepsubN  34056  pmaple  34065  pmapat  34067  pmap1N  34071  pmapsub  34072  pmapglbx  34073  isline2  34078  linepmap  34079  isline3  34080  isline4N  34081  lneq2at  34082  lncvrelatN  34085  lncmp  34087  2lnat  34088  2atm2atN  34089  2llnma1b  34090  2llnma1  34091  2llnma3r  34092  cdlema1N  34095  cdlemblem  34097  cdlemb  34098  elpaddn0  34104  paddcom  34117  paddasslem2  34125  paddasslem5  34128  paddasslem12  34135  paddasslem13  34136  pmapjoin  34156  pmapjat1  34157  pmapjat2  34158  pmapjlln1  34159  atmod1i1  34161  atmod1i2  34163  llnmod1i2  34164  atmod2i1  34165  atmod2i2  34166  atmod3i1  34168  atmod3i2  34169  atmod4i1  34170  atmod4i2  34171  llnexchb2lem  34172  llnexchb2  34173  dalawlem2  34176  dalawlem3  34177  dalawlem5  34179  dalawlem6  34180  dalawlem7  34181  dalawlem8  34182  dalawlem11  34185  dalawlem12  34186  polval2N  34210  pol1N  34214  polatN  34235  2polatN  34236  paddatclN  34253  linepsubclN  34255  lhp2lt  34305  lhp0lt  34307  lhpexle2lem  34313  lhpexle3lem  34315  lhpjat2  34325  lhpj1  34326  lhpmcvr3  34329  lhpmcvr4N  34330  lhpmcvr5N  34331  lhpmcvr6N  34332  lhpmatb  34335  lhp2at0  34336  lhp2atnle  34337  lhp2at0nle  34339  lhprelat3N  34344  lhple  34346  lhpat4N  34348  lhpat3  34350  4atexlemtlw  34371  4atexlemc  34373  4atexlemnclw  34374  4atexlemcnd  34376  4atex2-0aOLDN  34382  lauteq  34399  ltrnid  34439  ltrnel  34443  ltrnat  34444  ltrncnvat  34445  ltrncnvel  34446  ltrncoval  34449  ltrncnv  34450  ltrn11at  34451  ltrneq2  34452  ltrneq  34453  idltrn  34454  ltrnmwOLD  34456  trlval2  34468  trlcnv  34470  trljat1  34471  trljat2  34472  ltrnideq  34480  arglem1N  34495  cdlemc1  34496  cdlemc2  34497  cdlemc4  34499  cdlemc5  34500  cdlemc6  34501  cdlemd1  34503  cdlemd2  34504  cdlemd3  34505  cdlemd4  34506  cdlemd7  34509  cdleme0aa  34515  cdleme0b  34517  cdleme0c  34518  cdleme0cp  34519  cdleme0cq  34520  cdleme0e  34522  cdleme0fN  34523  cdleme1b  34531  cdleme1  34532  cdleme2  34533  cdleme3b  34534  cdleme3c  34535  cdleme3e  34537  cdleme3g  34539  cdleme3h  34540  cdleme3  34542  cdleme5  34545  cdleme7d  34551  cdleme7e  34552  cdleme7ga  34553  cdleme7  34554  cdleme8  34555  cdleme9  34558  cdleme10  34559  cdleme11c  34566  cdleme11e  34568  cdleme11fN  34569  cdleme11g  34570  cdleme11k  34573  cdleme11  34575  cdleme15b  34580  cdleme15  34583  cdleme16b  34584  cdleme17b  34592  cdleme17c  34593  cdlemednpq  34604  cdleme20zN  34606  cdleme20yOLD  34608  cdleme19a  34609  cdleme20bN  34616  cdleme20d  34618  cdleme20j  34624  cdleme21c  34633  cdleme22aa  34645  cdleme22b  34647  cdleme22cN  34648  cdleme22d  34649  cdleme22e  34650  cdleme22eALTN  34651  cdleme23b  34656  cdleme23c  34657  cdleme27N  34675  cdleme28a  34676  cdleme30a  34684  cdlemefrs29pre00  34701  cdlemefrs29bpre0  34702  cdlemefrs29cpre1  34704  cdlemefrs32fva  34706  cdlemefrs32fva1  34707  cdlemefr32snb  34711  cdlemefs32snb  34721  cdleme32snb  34742  cdleme32fva  34743  cdleme32fva1  34744  cdleme32fvaw  34745  cdleme35a  34754  cdleme35fnpq  34755  cdleme35b  34756  cdleme35c  34757  cdleme35f  34760  cdleme42c  34778  cdleme42e  34785  cdleme42h  34788  cdleme42i  34789  cdleme42ke  34791  cdleme42keg  34792  cdleme42mgN  34794  cdleme17d4  34803  cdleme48fvg  34806  cdleme48bw  34808  cdlemeg46req  34835  cdleme50trn3  34859  cdlemf1  34867  cdlemf2  34868  trlord  34875  ltrniotacnvval  34888  cdlemg2fv2  34906  cdlemg2l  34909  cdlemg7fvbwN  34913  cdlemg4c  34918  cdlemg4  34923  cdlemg6c  34926  cdlemg8b  34934  cdlemg11b  34948  cdlemg13a  34957  cdlemg17a  34967  cdlemg17h  34974  cdlemg17  34983  cdlemg18b  34985  cdlemg19a  34989  cdlemg27a  34998  cdlemg27b  35002  cdlemg31a  35003  cdlemg31b  35004  cdlemg31d  35006  cdlemg33b0  35007  cdlemg33a  35012  cdlemg35  35019  trlcolem  35032  cdlemg42  35035  cdlemg44a  35037  cdlemg46  35041  cdlemh1  35121  cdlemh2  35122  cdlemh  35123  cdlemi1  35124  cdlemi  35126  cdlemk3  35139  cdlemk4  35140  cdlemkvcl  35148  cdlemk7  35154  cdlemk11  35155  cdlemk15  35161  cdlemk1u  35165  cdlemk7u  35176  cdlemk11u  35177  cdlemk37  35220  cdlemk39  35222  cdlemkid1  35228  cdlemkid2  35230  cdlemk48  35256  cdlemk50  35258  cdlemk51  35259  cdlemk52  35260  dia2dimlem1  35371  dia2dimlem2  35372  dia2dimlem3  35373  dia2dimlem5  35375  dia2dimlem7  35377  dia2dimlem9  35379  dia2dimlem10  35380  dia2dimlem12  35382  dia2dimlem13  35383  cdlemm10N  35425  cdlemn2  35502  cdlemn3  35504  cdlemn9  35512  cdlemn10  35513  dihjustlem  35523  dihord1  35525  dihord2pre2  35533  dihvalcqat  35546  dib2dim  35550  dih2dimb  35551  dih2dimbALTN  35552  dihord5apre  35569  dihglbcpreN  35607  dihmeetlem3N  35612  dihmeetlem6  35616  dihjatc1  35618  dihjatc2N  35619  dihjatc3  35620  dihmeetlem9N  35622  dihmeetlem10N  35623  dihmeetlem11N  35624  dihmeetlem13N  35626  dihmeetlem15N  35628  dihmeetlem16N  35629  dihmeetlem17N  35630  dihatexv2  35646  dihjatb  35723  dihjatc  35724  dihjatcclem1  35725  dihjatcclem2  35726  dihjatcclem4  35728  dihjat  35730  dihjat3  35739  dihjat5N  35744  dvh4dimat  35745