Theorem atbase 40439

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 32951 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 4285	. . . 4 ⊢ (𝑃 ∈ 𝐴 → ¬ 𝐴 = ∅)
2		atombase.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
3	2	eqeq1i 2765	. . . 4 ⊢ (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
4	1, 3	sylnib 331	. . 3 ⊢ (𝑃 ∈ 𝐴 → ¬ (Atoms‘𝐾) = ∅)
5		fvprc 6877	. . 3 ⊢ (¬ 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
6	4, 5	nsyl2 142	. 2 ⊢ (𝑃 ∈ 𝐴 → 𝐾 ∈ V)
7		atombase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2760	. . . 4 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		eqid 2760	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	isat 40436	. . 3 ⊢ (𝐾 ∈ V → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
11	10	simprbda 504	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐵)
12	6, 11	mpancom 701	1 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  Vcvv 3450  ∅c0 4278   class class class wbr 5102  ‘cfv 6538  Basecbs 17392  0.cp0 18600   ⋖ ccvr 40412  Atomscatm 40413

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-iota 6494  df-fun 6540  df-fv 6546  df-ats 40417

This theorem is used by:  atssbase  40440  0ltat  40441  leatb  40442  meetat  40446  atnle0  40459  atlen0  40460  atcmp  40461  atcvreq0  40464  atncvrN  40465  atnle  40467  atnem0  40468  atlatmstc  40469  atlatle  40470  cvlexch2  40479  cvlexchb1  40480  cvlexchb2  40481  cvlatexchb1  40484  cvlatexchb2  40485  cvlatexch1  40486  cvlatexch2  40487  cvlatexch3  40488  cvlcvr1  40489  cvlcvrp  40490  cvlatcvr1  40491  cvlatcvr2  40492  cvlsupr2  40493  cvlsupr7  40498  cvlsupr8  40499  hlatjcl  40517  hlatjcom  40518  hlatjidm  40519  hlatjass  40520  hlatj32  40522  hlatj4  40524  hlatlej1  40525  atnlej1  40529  atnlej2  40530  hlrelat5N  40551  hlrelat  40552  hlrelat2  40553  exatleN  40554  cvr2N  40561  hlrelat3  40562  cvrval3  40563  cvrval5  40565  cvrexchlem  40569  cvratlem  40571  cvrat  40572  atcvr0eq  40576  lnnat  40577  cvrat2  40579  atcvrneN  40580  atcvrj1  40581  atcvrj2b  40582  atltcvr  40585  atle  40586  atlelt  40588  2atlt  40589  atexchcvrN  40590  cvrat3  40592  cvrat4  40593  cvrat42  40594  2atjm  40595  atbtwn  40596  3noncolr2  40599  4noncolr3  40603  athgt  40606  3dim0  40607  3dimlem3a  40610  3dimlem3OLDN  40612  3dimlem4a  40613  3dimlem4OLDN  40615  3dim3  40619  2dim  40620  1cvratex  40623  1cvrjat  40625  1cvrat  40626  ps-1  40627  ps-2  40628  hlatexch3N  40630  hlatexch4  40631  ps-2b  40632  3atlem1  40633  3atlem2  40634  3atlem4  40636  3atlem5  40637  3atlem6  40638  3at  40640  islln3  40660  llnnleat  40663  llnn0  40666  llnle  40668  llnexatN  40671  llncmp  40672  2llnmat  40674  2at0mat0  40675  2atm  40677  ps-2c  40678  lplni2  40687  lplnle  40690  lplnnle2at  40691  lplnn0N  40697  islpln2a  40698  2atmat  40711  lplnexllnN  40714  2llnjaN  40716  2llnm4  40720  2llnmeqat  40721  lvoli3  40727  islvol5  40729  lvoli2  40731  lvolnle3at  40732  3atnelvolN  40736  lvoln0N  40741  islvol2aN  40742  4atlem3  40746  4atlem3a  40747  4atlem3b  40748  4atlem4a  40749  4atlem4b  40750  4atlem4c  40751  4atlem4d  40752  4atlem9  40753  4atlem10a  40754  4atlem10  40756  4atlem11a  40757  4atlem11b  40758  4atlem11  40759  4atlem12a  40760  4atlem12b  40761  4atlem12  40762  4at2  40764  lplncvrlvol2  40765  2lplnja  40769  dalempeb  40789  dalemqeb  40790  dalemreb  40791  dalemseb  40792  dalemteb  40793  dalemueb  40794  dalem3  40814  dalem16  40829  dalemcceb  40839  dalem21  40844  dalem25  40848  dalem38  40860  dalem39  40861  dalem43  40865  dalem44  40866  dalem45  40867  dalem53  40875  dalem54  40876  dalem55  40877  dalem57  40879  dalem60  40882  snatpsubN  40900  linepsubN  40902  pmaple  40911  pmapat  40913  pmap1N  40917  pmapsub  40918  pmapglbx  40919  isline2  40924  linepmap  40925  isline3  40926  isline4N  40927  lneq2at  40928  lncvrelatN  40931  lncmp  40933  2lnat  40934  2atm2atN  40935  2llnma1b  40936  2llnma1  40937  2llnma3r  40938  cdlema1N  40941  cdlemblem  40943  cdlemb  40944  elpaddn0  40950  paddcom  40963  paddasslem2  40971  paddasslem5  40974  paddasslem12  40981  paddasslem13  40982  pmapjoin  41002  pmapjat1  41003  pmapjat2  41004  pmapjlln1  41005  atmod1i1  41007  atmod1i2  41009  llnmod1i2  41010  atmod2i1  41011  atmod2i2  41012  atmod3i1  41014  atmod3i2  41015  atmod4i1  41016  atmod4i2  41017  llnexchb2lem  41018  llnexchb2  41019  dalawlem2  41022  dalawlem3  41023  dalawlem5  41025  dalawlem6  41026  dalawlem7  41027  dalawlem8  41028  dalawlem11  41031  dalawlem12  41032  polval2N  41056  pol1N  41060  polatN  41081  2polatN  41082  paddatclN  41099  linepsubclN  41101  lhp2lt  41151  lhp0lt  41153  lhpexle2lem  41159  lhpexle3lem  41161  lhpjat2  41171  lhpj1  41172  lhpmcvr3  41175  lhpmcvr4N  41176  lhpmcvr5N  41177  lhpmcvr6N  41178  lhpmatb  41181  lhp2at0  41182  lhp2atnle  41183  lhp2at0nle  41185  lhprelat3N  41190  lhple  41192  lhpat4N  41194  lhpat3  41196  4atexlemtlw  41217  4atexlemc  41219  4atexlemnclw  41220  4atexlemcnd  41222  4atex2-0aOLDN  41228  lauteq  41245  ltrnid  41285  ltrnel  41289  ltrnat  41290  ltrncnvat  41291  ltrncnvel  41292  ltrncoval  41295  ltrncnv  41296  ltrn11at  41297  ltrneq2  41298  ltrneq  41299  idltrn  41300  trlval2  41313  trlcnv  41315  trljat1  41316  trljat2  41317  ltrnideq  41325  arglem1N  41340  cdlemc1  41341  cdlemc2  41342  cdlemc4  41344  cdlemc5  41345  cdlemc6  41346  cdlemd1  41348  cdlemd2  41349  cdlemd3  41350  cdlemd4  41351  cdlemd7  41354  cdleme0aa  41360  cdleme0b  41362  cdleme0c  41363  cdleme0cp  41364  cdleme0cq  41365  cdleme0e  41367  cdleme0fN  41368  cdleme1b  41376  cdleme1  41377  cdleme2  41378  cdleme3b  41379  cdleme3c  41380  cdleme3e  41382  cdleme3g  41384  cdleme3h  41385  cdleme3  41387  cdleme5  41390  cdleme7d  41396  cdleme7e  41397  cdleme7ga  41398  cdleme7  41399  cdleme8  41400  cdleme9  41403  cdleme10  41404  cdleme11c  41411  cdleme11e  41413  cdleme11fN  41414  cdleme11g  41415  cdleme11k  41418  cdleme11  41420  cdleme15b  41425  cdleme15  41428  cdleme16b  41429  cdleme17b  41437  cdleme17c  41438  cdlemednpq  41449  cdleme20zN  41451  cdleme19a  41453  cdleme20bN  41460  cdleme20d  41462  cdleme20j  41468  cdleme21c  41477  cdleme22aa  41489  cdleme22b  41491  cdleme22cN  41492  cdleme22d  41493  cdleme22e  41494  cdleme22eALTN  41495  cdleme23b  41500  cdleme23c  41501  cdleme27N  41519  cdleme28a  41520  cdleme30a  41528  cdlemefrs29pre00  41545  cdlemefrs29bpre0  41546  cdlemefrs29cpre1  41548  cdlemefrs32fva  41550  cdlemefrs32fva1  41551  cdlemefr32snb  41555  cdlemefs32snb  41565  cdleme32snb  41586  cdleme32fva  41587  cdleme32fva1  41588  cdleme32fvaw  41589  cdleme35a  41598  cdleme35fnpq  41599  cdleme35b  41600  cdleme35c  41601  cdleme35f  41604  cdleme42c  41622  cdleme42e  41629  cdleme42h  41632  cdleme42i  41633  cdleme42ke  41635  cdleme42keg  41636  cdleme42mgN  41638  cdleme17d4  41647  cdleme48fvg  41650  cdleme48bw  41652  cdlemeg46req  41679  cdleme50trn3  41703  cdlemf1  41711  cdlemf2  41712  trlord  41719  ltrniotacnvval  41732  cdlemg2fv2  41750  cdlemg2l  41753  cdlemg7fvbwN  41757  cdlemg4c  41762  cdlemg4  41767  cdlemg6c  41770  cdlemg8b  41778  cdlemg11b  41792  cdlemg13a  41801  cdlemg17a  41811  cdlemg17h  41818  cdlemg17  41827  cdlemg18b  41829  cdlemg19a  41833  cdlemg27a  41842  cdlemg27b  41846  cdlemg31a  41847  cdlemg31b  41848  cdlemg31d  41850  cdlemg33b0  41851  cdlemg33a  41856  cdlemg35  41863  trlcolem  41876  cdlemg42  41879  cdlemg44a  41881  cdlemg46  41885  cdlemh1  41965  cdlemh2  41966  cdlemh  41967  cdlemi1  41968  cdlemi  41970  cdlemk3  41983  cdlemk4  41984  cdlemkvcl  41992  cdlemk7  41998  cdlemk11  41999  cdlemk15  42005  cdlemk1u  42009  cdlemk7u  42020  cdlemk11u  42021  cdlemk37  42064  cdlemk39  42066  cdlemkid1  42072  cdlemkid2  42074  cdlemk48  42100  cdlemk50  42102  cdlemk51  42103  cdlemk52  42104  dia2dimlem1  42214  dia2dimlem2  42215  dia2dimlem3  42216  dia2dimlem5  42218  dia2dimlem7  42220  dia2dimlem9  42222  dia2dimlem10  42223  dia2dimlem12  42225  dia2dimlem13  42226  cdlemm10N  42268  cdlemn2  42345  cdlemn3  42347  cdlemn9  42355  cdlemn10  42356  dihjustlem  42366  dihord1  42368  dihord2pre2  42376  dihvalcqat  42389  dib2dim  42393  dih2dimb  42394  dih2dimbALTN  42395  dihord5apre  42412  dihglbcpreN  42450  dihmeetlem3N  42455  dihmeetlem6  42459  dihjatc1  42461  dihjatc2N  42462  dihjatc3  42463  dihmeetlem9N  42465  dihmeetlem10N  42466  dihmeetlem11N  42467  dihmeetlem13N  42469  dihmeetlem15N  42471  dihmeetlem16N  42472  dihmeetlem17N  42473  dihatexv2  42489  dihjatb  42566  dihjatc  42567  dihjatcclem1  42568  dihjatcclem2  42569  dihjatcclem4  42571  dihjat  42573  dihjat3  42582  dihjat5N  42587  dvh4dimat  42588