Theorem atbase 37230

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  Vcvv 3422  ∅c0 4253   class class class wbr 5070  ‘cfv 6418  Basecbs 16840  0.cp0 18056   ⋖ ccvr 37203  Atomscatm 37204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-iota 6376  df-fun 6420  df-fv 6426  df-ats 37208

This theorem is referenced by:  atssbase  37231  0ltat  37232  leatb  37233  meetat  37237  atnle0  37250  atlen0  37251  atcmp  37252  atcvreq0  37255  atncvrN  37256  atnle  37258  atnem0  37259  atlatmstc  37260  atlatle  37261  cvlexch2  37270  cvlexchb1  37271  cvlexchb2  37272  cvlatexchb1  37275  cvlatexchb2  37276  cvlatexch1  37277  cvlatexch2  37278  cvlatexch3  37279  cvlcvr1  37280  cvlcvrp  37281  cvlatcvr1  37282  cvlatcvr2  37283  cvlsupr2  37284  cvlsupr7  37289  cvlsupr8  37290  hlatjcl  37308  hlatjcom  37309  hlatjidm  37310  hlatjass  37311  hlatj32  37313  hlatj4  37315  hlatlej1  37316  atnlej1  37320  atnlej2  37321  hlrelat5N  37342  hlrelat  37343  hlrelat2  37344  exatleN  37345  cvr2N  37352  hlrelat3  37353  cvrval3  37354  cvrval5  37356  cvrexchlem  37360  cvratlem  37362  cvrat  37363  atcvr0eq  37367  lnnat  37368  cvrat2  37370  atcvrneN  37371  atcvrj1  37372  atcvrj2b  37373  atltcvr  37376  atle  37377  atlelt  37379  2atlt  37380  atexchcvrN  37381  cvrat3  37383  cvrat4  37384  cvrat42  37385  2atjm  37386  atbtwn  37387  3noncolr2  37390  4noncolr3  37394  athgt  37397  3dim0  37398  3dimlem3a  37401  3dimlem3OLDN  37403  3dimlem4a  37404  3dimlem4OLDN  37406  3dim3  37410  2dim  37411  1cvratex  37414  1cvrjat  37416  1cvrat  37417  ps-1  37418  ps-2  37419  hlatexch3N  37421  hlatexch4  37422  ps-2b  37423  3atlem1  37424  3atlem2  37425  3atlem4  37427  3atlem5  37428  3atlem6  37429  3at  37431  islln3  37451  llnnleat  37454  llnn0  37457  llnle  37459  llnexatN  37462  llncmp  37463  2llnmat  37465  2at0mat0  37466  2atm  37468  ps-2c  37469  lplni2  37478  lplnle  37481  lplnnle2at  37482  lplnn0N  37488  islpln2a  37489  2atmat  37502  lplnexllnN  37505  2llnjaN  37507  2llnm4  37511  2llnmeqat  37512  lvoli3  37518  islvol5  37520  lvoli2  37522  lvolnle3at  37523  3atnelvolN  37527  lvoln0N  37532  islvol2aN  37533  4atlem3  37537  4atlem3a  37538  4atlem3b  37539  4atlem4a  37540  4atlem4b  37541  4atlem4c  37542  4atlem4d  37543  4atlem9  37544  4atlem10a  37545  4atlem10  37547  4atlem11a  37548  4atlem11b  37549  4atlem11  37550  4atlem12a  37551  4atlem12b  37552  4atlem12  37553  4at2  37555  lplncvrlvol2  37556  2lplnja  37560  dalempeb  37580  dalemqeb  37581  dalemreb  37582  dalemseb  37583  dalemteb  37584  dalemueb  37585  dalem3  37605  dalem16  37620  dalemcceb  37630  dalem21  37635  dalem25  37639  dalem38  37651  dalem39  37652  dalem43  37656  dalem44  37657  dalem45  37658  dalem53  37666  dalem54  37667  dalem55  37668  dalem57  37670  dalem60  37673  snatpsubN  37691  linepsubN  37693  pmaple  37702  pmapat  37704  pmap1N  37708  pmapsub  37709  pmapglbx  37710  isline2  37715  linepmap  37716  isline3  37717  isline4N  37718  lneq2at  37719  lncvrelatN  37722  lncmp  37724  2lnat  37725  2atm2atN  37726  2llnma1b  37727  2llnma1  37728  2llnma3r  37729  cdlema1N  37732  cdlemblem  37734  cdlemb  37735  elpaddn0  37741  paddcom  37754  paddasslem2  37762  paddasslem5  37765  paddasslem12  37772  paddasslem13  37773  pmapjoin  37793  pmapjat1  37794  pmapjat2  37795  pmapjlln1  37796  atmod1i1  37798  atmod1i2  37800  llnmod1i2  37801  atmod2i1  37802  atmod2i2  37803  atmod3i1  37805  atmod3i2  37806  atmod4i1  37807  atmod4i2  37808  llnexchb2lem  37809  llnexchb2  37810  dalawlem2  37813  dalawlem3  37814  dalawlem5  37816  dalawlem6  37817  dalawlem7  37818  dalawlem8  37819  dalawlem11  37822  dalawlem12  37823  polval2N  37847  pol1N  37851  polatN  37872  2polatN  37873  paddatclN  37890  linepsubclN  37892  lhp2lt  37942  lhp0lt  37944  lhpexle2lem  37950  lhpexle3lem  37952  lhpjat2  37962  lhpj1  37963  lhpmcvr3  37966  lhpmcvr4N  37967  lhpmcvr5N  37968  lhpmcvr6N  37969  lhpmatb  37972  lhp2at0  37973  lhp2atnle  37974  lhp2at0nle  37976  lhprelat3N  37981  lhple  37983  lhpat4N  37985  lhpat3  37987  4atexlemtlw  38008  4atexlemc  38010  4atexlemnclw  38011  4atexlemcnd  38013  4atex2-0aOLDN  38019  lauteq  38036  ltrnid  38076  ltrnel  38080  ltrnat  38081  ltrncnvat  38082  ltrncnvel  38083  ltrncoval  38086  ltrncnv  38087  ltrn11at  38088  ltrneq2  38089  ltrneq  38090  idltrn  38091  trlval2  38104  trlcnv  38106  trljat1  38107  trljat2  38108  ltrnideq  38116  arglem1N  38131  cdlemc1  38132  cdlemc2  38133  cdlemc4  38135  cdlemc5  38136  cdlemc6  38137  cdlemd1  38139  cdlemd2  38140  cdlemd3  38141  cdlemd4  38142  cdlemd7  38145  cdleme0aa  38151  cdleme0b  38153  cdleme0c  38154  cdleme0cp  38155  cdleme0cq  38156  cdleme0e  38158  cdleme0fN  38159  cdleme1b  38167  cdleme1  38168  cdleme2  38169  cdleme3b  38170  cdleme3c  38171  cdleme3e  38173  cdleme3g  38175  cdleme3h  38176  cdleme3  38178  cdleme5  38181  cdleme7d  38187  cdleme7e  38188  cdleme7ga  38189  cdleme7  38190  cdleme8  38191  cdleme9  38194  cdleme10  38195  cdleme11c  38202  cdleme11e  38204  cdleme11fN  38205  cdleme11g  38206  cdleme11k  38209  cdleme11  38211  cdleme15b  38216  cdleme15  38219  cdleme16b  38220  cdleme17b  38228  cdleme17c  38229  cdlemednpq  38240  cdleme20zN  38242  cdleme19a  38244  cdleme20bN  38251  cdleme20d  38253  cdleme20j  38259  cdleme21c  38268  cdleme22aa  38280  cdleme22b  38282  cdleme22cN  38283  cdleme22d  38284  cdleme22e  38285  cdleme22eALTN  38286  cdleme23b  38291  cdleme23c  38292  cdleme27N  38310  cdleme28a  38311  cdleme30a  38319  cdlemefrs29pre00  38336  cdlemefrs29bpre0  38337  cdlemefrs29cpre1  38339  cdlemefrs32fva  38341  cdlemefrs32fva1  38342  cdlemefr32snb  38346  cdlemefs32snb  38356  cdleme32snb  38377  cdleme32fva  38378  cdleme32fva1  38379  cdleme32fvaw  38380  cdleme35a  38389  cdleme35fnpq  38390  cdleme35b  38391  cdleme35c  38392  cdleme35f  38395  cdleme42c  38413  cdleme42e  38420  cdleme42h  38423  cdleme42i  38424  cdleme42ke  38426  cdleme42keg  38427  cdleme42mgN  38429  cdleme17d4  38438  cdleme48fvg  38441  cdleme48bw  38443  cdlemeg46req  38470  cdleme50trn3  38494  cdlemf1  38502  cdlemf2  38503  trlord  38510  ltrniotacnvval  38523  cdlemg2fv2  38541  cdlemg2l  38544  cdlemg7fvbwN  38548  cdlemg4c  38553  cdlemg4  38558  cdlemg6c  38561  cdlemg8b  38569  cdlemg11b  38583  cdlemg13a  38592  cdlemg17a  38602  cdlemg17h  38609  cdlemg17  38618  cdlemg18b  38620  cdlemg19a  38624  cdlemg27a  38633  cdlemg27b  38637  cdlemg31a  38638  cdlemg31b  38639  cdlemg31d  38641  cdlemg33b0  38642  cdlemg33a  38647  cdlemg35  38654  trlcolem  38667  cdlemg42  38670  cdlemg44a  38672  cdlemg46  38676  cdlemh1  38756  cdlemh2  38757  cdlemh  38758  cdlemi1  38759  cdlemi  38761  cdlemk3  38774  cdlemk4  38775  cdlemkvcl  38783  cdlemk7  38789  cdlemk11  38790  cdlemk15  38796  cdlemk1u  38800  cdlemk7u  38811  cdlemk11u  38812  cdlemk37  38855  cdlemk39  38857  cdlemkid1  38863  cdlemkid2  38865  cdlemk48  38891  cdlemk50  38893  cdlemk51  38894  cdlemk52  38895  dia2dimlem1  39005  dia2dimlem2  39006  dia2dimlem3  39007  dia2dimlem5  39009  dia2dimlem7  39011  dia2dimlem9  39013  dia2dimlem10  39014  dia2dimlem12  39016  dia2dimlem13  39017  cdlemm10N  39059  cdlemn2  39136  cdlemn3  39138  cdlemn9  39146  cdlemn10  39147  dihjustlem  39157  dihord1  39159  dihord2pre2  39167  dihvalcqat  39180  dib2dim  39184  dih2dimb  39185  dih2dimbALTN  39186  dihord5apre  39203  dihglbcpreN  39241  dihmeetlem3N  39246  dihmeetlem6  39250  dihjatc1  39252  dihjatc2N  39253  dihjatc3  39254  dihmeetlem9N  39256  dihmeetlem10N  39257  dihmeetlem11N  39258  dihmeetlem13N  39260  dihmeetlem15N  39262  dihmeetlem16N  39263  dihmeetlem17N  39264  dihatexv2  39280  dihjatb  39357  dihjatc  39358  dihjatcclem1  39359  dihjatcclem2  39360  dihjatcclem4  39362  dihjat  39364  dihjat3  39373  dihjat5N  39378  dvh4dimat  39379