Theorem atbase 36427

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 30123 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 4301	. . . 4 ⊢ (𝑃 ∈ 𝐴 → ¬ 𝐴 = ∅)
2		atombase.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
3	2	eqeq1i 2828	. . . 4 ⊢ (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
4	1, 3	sylnib 330	. . 3 ⊢ (𝑃 ∈ 𝐴 → ¬ (Atoms‘𝐾) = ∅)
5		fvprc 6665	. . 3 ⊢ (¬ 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
6	4, 5	nsyl2 143	. 2 ⊢ (𝑃 ∈ 𝐴 → 𝐾 ∈ V)
7		atombase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2823	. . . 4 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		eqid 2823	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	isat 36424	. . 3 ⊢ (𝐾 ∈ V → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
11	10	simprbda 501	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐵)
12	6, 11	mpancom 686	1 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  Vcvv 3496  ∅c0 4293   class class class wbr 5068  ‘cfv 6357  Basecbs 16485  0.cp0 17649   ⋖ ccvr 36400  Atomscatm 36401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-iota 6316  df-fun 6359  df-fv 6365  df-ats 36405

This theorem is referenced by:  atssbase  36428  0ltat  36429  leatb  36430  meetat  36434  atnle0  36447  atlen0  36448  atcmp  36449  atcvreq0  36452  atncvrN  36453  atnle  36455  atnem0  36456  atlatmstc  36457  atlatle  36458  cvlexch2  36467  cvlexchb1  36468  cvlexchb2  36469  cvlatexchb1  36472  cvlatexchb2  36473  cvlatexch1  36474  cvlatexch2  36475  cvlatexch3  36476  cvlcvr1  36477  cvlcvrp  36478  cvlatcvr1  36479  cvlatcvr2  36480  cvlsupr2  36481  cvlsupr7  36486  cvlsupr8  36487  hlatjcl  36505  hlatjcom  36506  hlatjidm  36507  hlatjass  36508  hlatj32  36510  hlatj4  36512  hlatlej1  36513  atnlej1  36517  atnlej2  36518  hlrelat5N  36539  hlrelat  36540  hlrelat2  36541  exatleN  36542  cvr2N  36549  hlrelat3  36550  cvrval3  36551  cvrval5  36553  cvrexchlem  36557  cvratlem  36559  cvrat  36560  atcvr0eq  36564  lnnat  36565  cvrat2  36567  atcvrneN  36568  atcvrj1  36569  atcvrj2b  36570  atltcvr  36573  atle  36574  atlelt  36576  2atlt  36577  atexchcvrN  36578  cvrat3  36580  cvrat4  36581  cvrat42  36582  2atjm  36583  atbtwn  36584  3noncolr2  36587  4noncolr3  36591  athgt  36594  3dim0  36595  3dimlem3a  36598  3dimlem3OLDN  36600  3dimlem4a  36601  3dimlem4OLDN  36603  3dim3  36607  2dim  36608  1cvratex  36611  1cvrjat  36613  1cvrat  36614  ps-1  36615  ps-2  36616  hlatexch3N  36618  hlatexch4  36619  ps-2b  36620  3atlem1  36621  3atlem2  36622  3atlem4  36624  3atlem5  36625  3atlem6  36626  3at  36628  islln3  36648  llnnleat  36651  llnn0  36654  llnle  36656  llnexatN  36659  llncmp  36660  2llnmat  36662  2at0mat0  36663  2atm  36665  ps-2c  36666  lplni2  36675  lplnle  36678  lplnnle2at  36679  lplnn0N  36685  islpln2a  36686  2atmat  36699  lplnexllnN  36702  2llnjaN  36704  2llnm4  36708  2llnmeqat  36709  lvoli3  36715  islvol5  36717  lvoli2  36719  lvolnle3at  36720  3atnelvolN  36724  lvoln0N  36729  islvol2aN  36730  4atlem3  36734  4atlem3a  36735  4atlem3b  36736  4atlem4a  36737  4atlem4b  36738  4atlem4c  36739  4atlem4d  36740  4atlem9  36741  4atlem10a  36742  4atlem10  36744  4atlem11a  36745  4atlem11b  36746  4atlem11  36747  4atlem12a  36748  4atlem12b  36749  4atlem12  36750  4at2  36752  lplncvrlvol2  36753  2lplnja  36757  dalempeb  36777  dalemqeb  36778  dalemreb  36779  dalemseb  36780  dalemteb  36781  dalemueb  36782  dalem3  36802  dalem16  36817  dalemcceb  36827  dalem21  36832  dalem25  36836  dalem38  36848  dalem39  36849  dalem43  36853  dalem44  36854  dalem45  36855  dalem53  36863  dalem54  36864  dalem55  36865  dalem57  36867  dalem60  36870  snatpsubN  36888  linepsubN  36890  pmaple  36899  pmapat  36901  pmap1N  36905  pmapsub  36906  pmapglbx  36907  isline2  36912  linepmap  36913  isline3  36914  isline4N  36915  lneq2at  36916  lncvrelatN  36919  lncmp  36921  2lnat  36922  2atm2atN  36923  2llnma1b  36924  2llnma1  36925  2llnma3r  36926  cdlema1N  36929  cdlemblem  36931  cdlemb  36932  elpaddn0  36938  paddcom  36951  paddasslem2  36959  paddasslem5  36962  paddasslem12  36969  paddasslem13  36970  pmapjoin  36990  pmapjat1  36991  pmapjat2  36992  pmapjlln1  36993  atmod1i1  36995  atmod1i2  36997  llnmod1i2  36998  atmod2i1  36999  atmod2i2  37000  atmod3i1  37002  atmod3i2  37003  atmod4i1  37004  atmod4i2  37005  llnexchb2lem  37006  llnexchb2  37007  dalawlem2  37010  dalawlem3  37011  dalawlem5  37013  dalawlem6  37014  dalawlem7  37015  dalawlem8  37016  dalawlem11  37019  dalawlem12  37020  polval2N  37044  pol1N  37048  polatN  37069  2polatN  37070  paddatclN  37087  linepsubclN  37089  lhp2lt  37139  lhp0lt  37141  lhpexle2lem  37147  lhpexle3lem  37149  lhpjat2  37159  lhpj1  37160  lhpmcvr3  37163  lhpmcvr4N  37164  lhpmcvr5N  37165  lhpmcvr6N  37166  lhpmatb  37169  lhp2at0  37170  lhp2atnle  37171  lhp2at0nle  37173  lhprelat3N  37178  lhple  37180  lhpat4N  37182  lhpat3  37184  4atexlemtlw  37205  4atexlemc  37207  4atexlemnclw  37208  4atexlemcnd  37210  4atex2-0aOLDN  37216  lauteq  37233  ltrnid  37273  ltrnel  37277  ltrnat  37278  ltrncnvat  37279  ltrncnvel  37280  ltrncoval  37283  ltrncnv  37284  ltrn11at  37285  ltrneq2  37286  ltrneq  37287  idltrn  37288  trlval2  37301  trlcnv  37303  trljat1  37304  trljat2  37305  ltrnideq  37313  arglem1N  37328  cdlemc1  37329  cdlemc2  37330  cdlemc4  37332  cdlemc5  37333  cdlemc6  37334  cdlemd1  37336  cdlemd2  37337  cdlemd3  37338  cdlemd4  37339  cdlemd7  37342  cdleme0aa  37348  cdleme0b  37350  cdleme0c  37351  cdleme0cp  37352  cdleme0cq  37353  cdleme0e  37355  cdleme0fN  37356  cdleme1b  37364  cdleme1  37365  cdleme2  37366  cdleme3b  37367  cdleme3c  37368  cdleme3e  37370  cdleme3g  37372  cdleme3h  37373  cdleme3  37375  cdleme5  37378  cdleme7d  37384  cdleme7e  37385  cdleme7ga  37386  cdleme7  37387  cdleme8  37388  cdleme9  37391  cdleme10  37392  cdleme11c  37399  cdleme11e  37401  cdleme11fN  37402  cdleme11g  37403  cdleme11k  37406  cdleme11  37408  cdleme15b  37413  cdleme15  37416  cdleme16b  37417  cdleme17b  37425  cdleme17c  37426  cdlemednpq  37437  cdleme20zN  37439  cdleme19a  37441  cdleme20bN  37448  cdleme20d  37450  cdleme20j  37456  cdleme21c  37465  cdleme22aa  37477  cdleme22b  37479  cdleme22cN  37480  cdleme22d  37481  cdleme22e  37482  cdleme22eALTN  37483  cdleme23b  37488  cdleme23c  37489  cdleme27N  37507  cdleme28a  37508  cdleme30a  37516  cdlemefrs29pre00  37533  cdlemefrs29bpre0  37534  cdlemefrs29cpre1  37536  cdlemefrs32fva  37538  cdlemefrs32fva1  37539  cdlemefr32snb  37543  cdlemefs32snb  37553  cdleme32snb  37574  cdleme32fva  37575  cdleme32fva1  37576  cdleme32fvaw  37577  cdleme35a  37586  cdleme35fnpq  37587  cdleme35b  37588  cdleme35c  37589  cdleme35f  37592  cdleme42c  37610  cdleme42e  37617  cdleme42h  37620  cdleme42i  37621  cdleme42ke  37623  cdleme42keg  37624  cdleme42mgN  37626  cdleme17d4  37635  cdleme48fvg  37638  cdleme48bw  37640  cdlemeg46req  37667  cdleme50trn3  37691  cdlemf1  37699  cdlemf2  37700  trlord  37707  ltrniotacnvval  37720  cdlemg2fv2  37738  cdlemg2l  37741  cdlemg7fvbwN  37745  cdlemg4c  37750  cdlemg4  37755  cdlemg6c  37758  cdlemg8b  37766  cdlemg11b  37780  cdlemg13a  37789  cdlemg17a  37799  cdlemg17h  37806  cdlemg17  37815  cdlemg18b  37817  cdlemg19a  37821  cdlemg27a  37830  cdlemg27b  37834  cdlemg31a  37835  cdlemg31b  37836  cdlemg31d  37838  cdlemg33b0  37839  cdlemg33a  37844  cdlemg35  37851  trlcolem  37864  cdlemg42  37867  cdlemg44a  37869  cdlemg46  37873  cdlemh1  37953  cdlemh2  37954  cdlemh  37955  cdlemi1  37956  cdlemi  37958  cdlemk3  37971  cdlemk4  37972  cdlemkvcl  37980  cdlemk7  37986  cdlemk11  37987  cdlemk15  37993  cdlemk1u  37997  cdlemk7u  38008  cdlemk11u  38009  cdlemk37  38052  cdlemk39  38054  cdlemkid1  38060  cdlemkid2  38062  cdlemk48  38088  cdlemk50  38090  cdlemk51  38091  cdlemk52  38092  dia2dimlem1  38202  dia2dimlem2  38203  dia2dimlem3  38204  dia2dimlem5  38206  dia2dimlem7  38208  dia2dimlem9  38210  dia2dimlem10  38211  dia2dimlem12  38213  dia2dimlem13  38214  cdlemm10N  38256  cdlemn2  38333  cdlemn3  38335  cdlemn9  38343  cdlemn10  38344  dihjustlem  38354  dihord1  38356  dihord2pre2  38364  dihvalcqat  38377  dib2dim  38381  dih2dimb  38382  dih2dimbALTN  38383  dihord5apre  38400  dihglbcpreN  38438  dihmeetlem3N  38443  dihmeetlem6  38447  dihjatc1  38449  dihjatc2N  38450  dihjatc3  38451  dihmeetlem9N  38453  dihmeetlem10N  38454  dihmeetlem11N  38455  dihmeetlem13N  38457  dihmeetlem15N  38459  dihmeetlem16N  38460  dihmeetlem17N  38461  dihatexv2  38477  dihjatb  38554  dihjatc  38555  dihjatcclem1  38556  dihjatcclem2  38557  dihjatcclem4  38559  dihjat  38561  dihjat3  38570  dihjat5N  38575  dvh4dimat  38576