Theorem atbase 39272

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 32288 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 4291	. . . 4 ⊢ (𝑃 ∈ 𝐴 → ¬ 𝐴 = ∅)
2		atombase.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
3	2	eqeq1i 2734	. . . 4 ⊢ (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
4	1, 3	sylnib 328	. . 3 ⊢ (𝑃 ∈ 𝐴 → ¬ (Atoms‘𝐾) = ∅)
5		fvprc 6814	. . 3 ⊢ (¬ 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
6	4, 5	nsyl2 141	. 2 ⊢ (𝑃 ∈ 𝐴 → 𝐾 ∈ V)
7		atombase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2729	. . . 4 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		eqid 2729	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	isat 39269	. . 3 ⊢ (𝐾 ∈ V → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
11	10	simprbda 498	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐵)
12	6, 11	mpancom 688	1 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3436  ∅c0 4284   class class class wbr 5092  ‘cfv 6482  Basecbs 17120  0.cp0 18327   ⋖ ccvr 39245  Atomscatm 39246

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6438  df-fun 6484  df-fv 6490  df-ats 39250

This theorem is referenced by:  atssbase  39273  0ltat  39274  leatb  39275  meetat  39279  atnle0  39292  atlen0  39293  atcmp  39294  atcvreq0  39297  atncvrN  39298  atnle  39300  atnem0  39301  atlatmstc  39302  atlatle  39303  cvlexch2  39312  cvlexchb1  39313  cvlexchb2  39314  cvlatexchb1  39317  cvlatexchb2  39318  cvlatexch1  39319  cvlatexch2  39320  cvlatexch3  39321  cvlcvr1  39322  cvlcvrp  39323  cvlatcvr1  39324  cvlatcvr2  39325  cvlsupr2  39326  cvlsupr7  39331  cvlsupr8  39332  hlatjcl  39350  hlatjcom  39351  hlatjidm  39352  hlatjass  39353  hlatj32  39355  hlatj4  39357  hlatlej1  39358  atnlej1  39362  atnlej2  39363  hlrelat5N  39384  hlrelat  39385  hlrelat2  39386  exatleN  39387  cvr2N  39394  hlrelat3  39395  cvrval3  39396  cvrval5  39398  cvrexchlem  39402  cvratlem  39404  cvrat  39405  atcvr0eq  39409  lnnat  39410  cvrat2  39412  atcvrneN  39413  atcvrj1  39414  atcvrj2b  39415  atltcvr  39418  atle  39419  atlelt  39421  2atlt  39422  atexchcvrN  39423  cvrat3  39425  cvrat4  39426  cvrat42  39427  2atjm  39428  atbtwn  39429  3noncolr2  39432  4noncolr3  39436  athgt  39439  3dim0  39440  3dimlem3a  39443  3dimlem3OLDN  39445  3dimlem4a  39446  3dimlem4OLDN  39448  3dim3  39452  2dim  39453  1cvratex  39456  1cvrjat  39458  1cvrat  39459  ps-1  39460  ps-2  39461  hlatexch3N  39463  hlatexch4  39464  ps-2b  39465  3atlem1  39466  3atlem2  39467  3atlem4  39469  3atlem5  39470  3atlem6  39471  3at  39473  islln3  39493  llnnleat  39496  llnn0  39499  llnle  39501  llnexatN  39504  llncmp  39505  2llnmat  39507  2at0mat0  39508  2atm  39510  ps-2c  39511  lplni2  39520  lplnle  39523  lplnnle2at  39524  lplnn0N  39530  islpln2a  39531  2atmat  39544  lplnexllnN  39547  2llnjaN  39549  2llnm4  39553  2llnmeqat  39554  lvoli3  39560  islvol5  39562  lvoli2  39564  lvolnle3at  39565  3atnelvolN  39569  lvoln0N  39574  islvol2aN  39575  4atlem3  39579  4atlem3a  39580  4atlem3b  39581  4atlem4a  39582  4atlem4b  39583  4atlem4c  39584  4atlem4d  39585  4atlem9  39586  4atlem10a  39587  4atlem10  39589  4atlem11a  39590  4atlem11b  39591  4atlem11  39592  4atlem12a  39593  4atlem12b  39594  4atlem12  39595  4at2  39597  lplncvrlvol2  39598  2lplnja  39602  dalempeb  39622  dalemqeb  39623  dalemreb  39624  dalemseb  39625  dalemteb  39626  dalemueb  39627  dalem3  39647  dalem16  39662  dalemcceb  39672  dalem21  39677  dalem25  39681  dalem38  39693  dalem39  39694  dalem43  39698  dalem44  39699  dalem45  39700  dalem53  39708  dalem54  39709  dalem55  39710  dalem57  39712  dalem60  39715  snatpsubN  39733  linepsubN  39735  pmaple  39744  pmapat  39746  pmap1N  39750  pmapsub  39751  pmapglbx  39752  isline2  39757  linepmap  39758  isline3  39759  isline4N  39760  lneq2at  39761  lncvrelatN  39764  lncmp  39766  2lnat  39767  2atm2atN  39768  2llnma1b  39769  2llnma1  39770  2llnma3r  39771  cdlema1N  39774  cdlemblem  39776  cdlemb  39777  elpaddn0  39783  paddcom  39796  paddasslem2  39804  paddasslem5  39807  paddasslem12  39814  paddasslem13  39815  pmapjoin  39835  pmapjat1  39836  pmapjat2  39837  pmapjlln1  39838  atmod1i1  39840  atmod1i2  39842  llnmod1i2  39843  atmod2i1  39844  atmod2i2  39845  atmod3i1  39847  atmod3i2  39848  atmod4i1  39849  atmod4i2  39850  llnexchb2lem  39851  llnexchb2  39852  dalawlem2  39855  dalawlem3  39856  dalawlem5  39858  dalawlem6  39859  dalawlem7  39860  dalawlem8  39861  dalawlem11  39864  dalawlem12  39865  polval2N  39889  pol1N  39893  polatN  39914  2polatN  39915  paddatclN  39932  linepsubclN  39934  lhp2lt  39984  lhp0lt  39986  lhpexle2lem  39992  lhpexle3lem  39994  lhpjat2  40004  lhpj1  40005  lhpmcvr3  40008  lhpmcvr4N  40009  lhpmcvr5N  40010  lhpmcvr6N  40011  lhpmatb  40014  lhp2at0  40015  lhp2atnle  40016  lhp2at0nle  40018  lhprelat3N  40023  lhple  40025  lhpat4N  40027  lhpat3  40029  4atexlemtlw  40050  4atexlemc  40052  4atexlemnclw  40053  4atexlemcnd  40055  4atex2-0aOLDN  40061  lauteq  40078  ltrnid  40118  ltrnel  40122  ltrnat  40123  ltrncnvat  40124  ltrncnvel  40125  ltrncoval  40128  ltrncnv  40129  ltrn11at  40130  ltrneq2  40131  ltrneq  40132  idltrn  40133  trlval2  40146  trlcnv  40148  trljat1  40149  trljat2  40150  ltrnideq  40158  arglem1N  40173  cdlemc1  40174  cdlemc2  40175  cdlemc4  40177  cdlemc5  40178  cdlemc6  40179  cdlemd1  40181  cdlemd2  40182  cdlemd3  40183  cdlemd4  40184  cdlemd7  40187  cdleme0aa  40193  cdleme0b  40195  cdleme0c  40196  cdleme0cp  40197  cdleme0cq  40198  cdleme0e  40200  cdleme0fN  40201  cdleme1b  40209  cdleme1  40210  cdleme2  40211  cdleme3b  40212  cdleme3c  40213  cdleme3e  40215  cdleme3g  40217  cdleme3h  40218  cdleme3  40220  cdleme5  40223  cdleme7d  40229  cdleme7e  40230  cdleme7ga  40231  cdleme7  40232  cdleme8  40233  cdleme9  40236  cdleme10  40237  cdleme11c  40244  cdleme11e  40246  cdleme11fN  40247  cdleme11g  40248  cdleme11k  40251  cdleme11  40253  cdleme15b  40258  cdleme15  40261  cdleme16b  40262  cdleme17b  40270  cdleme17c  40271  cdlemednpq  40282  cdleme20zN  40284  cdleme19a  40286  cdleme20bN  40293  cdleme20d  40295  cdleme20j  40301  cdleme21c  40310  cdleme22aa  40322  cdleme22b  40324  cdleme22cN  40325  cdleme22d  40326  cdleme22e  40327  cdleme22eALTN  40328  cdleme23b  40333  cdleme23c  40334  cdleme27N  40352  cdleme28a  40353  cdleme30a  40361  cdlemefrs29pre00  40378  cdlemefrs29bpre0  40379  cdlemefrs29cpre1  40381  cdlemefrs32fva  40383  cdlemefrs32fva1  40384  cdlemefr32snb  40388  cdlemefs32snb  40398  cdleme32snb  40419  cdleme32fva  40420  cdleme32fva1  40421  cdleme32fvaw  40422  cdleme35a  40431  cdleme35fnpq  40432  cdleme35b  40433  cdleme35c  40434  cdleme35f  40437  cdleme42c  40455  cdleme42e  40462  cdleme42h  40465  cdleme42i  40466  cdleme42ke  40468  cdleme42keg  40469  cdleme42mgN  40471  cdleme17d4  40480  cdleme48fvg  40483  cdleme48bw  40485  cdlemeg46req  40512  cdleme50trn3  40536  cdlemf1  40544  cdlemf2  40545  trlord  40552  ltrniotacnvval  40565  cdlemg2fv2  40583  cdlemg2l  40586  cdlemg7fvbwN  40590  cdlemg4c  40595  cdlemg4  40600  cdlemg6c  40603  cdlemg8b  40611  cdlemg11b  40625  cdlemg13a  40634  cdlemg17a  40644  cdlemg17h  40651  cdlemg17  40660  cdlemg18b  40662  cdlemg19a  40666  cdlemg27a  40675  cdlemg27b  40679  cdlemg31a  40680  cdlemg31b  40681  cdlemg31d  40683  cdlemg33b0  40684  cdlemg33a  40689  cdlemg35  40696  trlcolem  40709  cdlemg42  40712  cdlemg44a  40714  cdlemg46  40718  cdlemh1  40798  cdlemh2  40799  cdlemh  40800  cdlemi1  40801  cdlemi  40803  cdlemk3  40816  cdlemk4  40817  cdlemkvcl  40825  cdlemk7  40831  cdlemk11  40832  cdlemk15  40838  cdlemk1u  40842  cdlemk7u  40853  cdlemk11u  40854  cdlemk37  40897  cdlemk39  40899  cdlemkid1  40905  cdlemkid2  40907  cdlemk48  40933  cdlemk50  40935  cdlemk51  40936  cdlemk52  40937  dia2dimlem1  41047  dia2dimlem2  41048  dia2dimlem3  41049  dia2dimlem5  41051  dia2dimlem7  41053  dia2dimlem9  41055  dia2dimlem10  41056  dia2dimlem12  41058  dia2dimlem13  41059  cdlemm10N  41101  cdlemn2  41178  cdlemn3  41180  cdlemn9  41188  cdlemn10  41189  dihjustlem  41199  dihord1  41201  dihord2pre2  41209  dihvalcqat  41222  dib2dim  41226  dih2dimb  41227  dih2dimbALTN  41228  dihord5apre  41245  dihglbcpreN  41283  dihmeetlem3N  41288  dihmeetlem6  41292  dihjatc1  41294  dihjatc2N  41295  dihjatc3  41296  dihmeetlem9N  41298  dihmeetlem10N  41299  dihmeetlem11N  41300  dihmeetlem13N  41302  dihmeetlem15N  41304  dihmeetlem16N  41305  dihmeetlem17N  41306  dihatexv2  41322  dihjatb  41399  dihjatc  41400  dihjatcclem1  41401  dihjatcclem2  41402  dihjatcclem4  41404  dihjat  41406  dihjat3  41415  dihjat5N  41420  dvh4dimat  41421