Theorem atbase 37310

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  Vcvv 3433  ∅c0 4257   class class class wbr 5075  ‘cfv 6437  Basecbs 16921  0.cp0 18150   ⋖ ccvr 37283  Atomscatm 37284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-iota 6395  df-fun 6439  df-fv 6445  df-ats 37288

This theorem is referenced by:  atssbase  37311  0ltat  37312  leatb  37313  meetat  37317  atnle0  37330  atlen0  37331  atcmp  37332  atcvreq0  37335  atncvrN  37336  atnle  37338  atnem0  37339  atlatmstc  37340  atlatle  37341  cvlexch2  37350  cvlexchb1  37351  cvlexchb2  37352  cvlatexchb1  37355  cvlatexchb2  37356  cvlatexch1  37357  cvlatexch2  37358  cvlatexch3  37359  cvlcvr1  37360  cvlcvrp  37361  cvlatcvr1  37362  cvlatcvr2  37363  cvlsupr2  37364  cvlsupr7  37369  cvlsupr8  37370  hlatjcl  37388  hlatjcom  37389  hlatjidm  37390  hlatjass  37391  hlatj32  37393  hlatj4  37395  hlatlej1  37396  atnlej1  37400  atnlej2  37401  hlrelat5N  37422  hlrelat  37423  hlrelat2  37424  exatleN  37425  cvr2N  37432  hlrelat3  37433  cvrval3  37434  cvrval5  37436  cvrexchlem  37440  cvratlem  37442  cvrat  37443  atcvr0eq  37447  lnnat  37448  cvrat2  37450  atcvrneN  37451  atcvrj1  37452  atcvrj2b  37453  atltcvr  37456  atle  37457  atlelt  37459  2atlt  37460  atexchcvrN  37461  cvrat3  37463  cvrat4  37464  cvrat42  37465  2atjm  37466  atbtwn  37467  3noncolr2  37470  4noncolr3  37474  athgt  37477  3dim0  37478  3dimlem3a  37481  3dimlem3OLDN  37483  3dimlem4a  37484  3dimlem4OLDN  37486  3dim3  37490  2dim  37491  1cvratex  37494  1cvrjat  37496  1cvrat  37497  ps-1  37498  ps-2  37499  hlatexch3N  37501  hlatexch4  37502  ps-2b  37503  3atlem1  37504  3atlem2  37505  3atlem4  37507  3atlem5  37508  3atlem6  37509  3at  37511  islln3  37531  llnnleat  37534  llnn0  37537  llnle  37539  llnexatN  37542  llncmp  37543  2llnmat  37545  2at0mat0  37546  2atm  37548  ps-2c  37549  lplni2  37558  lplnle  37561  lplnnle2at  37562  lplnn0N  37568  islpln2a  37569  2atmat  37582  lplnexllnN  37585  2llnjaN  37587  2llnm4  37591  2llnmeqat  37592  lvoli3  37598  islvol5  37600  lvoli2  37602  lvolnle3at  37603  3atnelvolN  37607  lvoln0N  37612  islvol2aN  37613  4atlem3  37617  4atlem3a  37618  4atlem3b  37619  4atlem4a  37620  4atlem4b  37621  4atlem4c  37622  4atlem4d  37623  4atlem9  37624  4atlem10a  37625  4atlem10  37627  4atlem11a  37628  4atlem11b  37629  4atlem11  37630  4atlem12a  37631  4atlem12b  37632  4atlem12  37633  4at2  37635  lplncvrlvol2  37636  2lplnja  37640  dalempeb  37660  dalemqeb  37661  dalemreb  37662  dalemseb  37663  dalemteb  37664  dalemueb  37665  dalem3  37685  dalem16  37700  dalemcceb  37710  dalem21  37715  dalem25  37719  dalem38  37731  dalem39  37732  dalem43  37736  dalem44  37737  dalem45  37738  dalem53  37746  dalem54  37747  dalem55  37748  dalem57  37750  dalem60  37753  snatpsubN  37771  linepsubN  37773  pmaple  37782  pmapat  37784  pmap1N  37788  pmapsub  37789  pmapglbx  37790  isline2  37795  linepmap  37796  isline3  37797  isline4N  37798  lneq2at  37799  lncvrelatN  37802  lncmp  37804  2lnat  37805  2atm2atN  37806  2llnma1b  37807  2llnma1  37808  2llnma3r  37809  cdlema1N  37812  cdlemblem  37814  cdlemb  37815  elpaddn0  37821  paddcom  37834  paddasslem2  37842  paddasslem5  37845  paddasslem12  37852  paddasslem13  37853  pmapjoin  37873  pmapjat1  37874  pmapjat2  37875  pmapjlln1  37876  atmod1i1  37878  atmod1i2  37880  llnmod1i2  37881  atmod2i1  37882  atmod2i2  37883  atmod3i1  37885  atmod3i2  37886  atmod4i1  37887  atmod4i2  37888  llnexchb2lem  37889  llnexchb2  37890  dalawlem2  37893  dalawlem3  37894  dalawlem5  37896  dalawlem6  37897  dalawlem7  37898  dalawlem8  37899  dalawlem11  37902  dalawlem12  37903  polval2N  37927  pol1N  37931  polatN  37952  2polatN  37953  paddatclN  37970  linepsubclN  37972  lhp2lt  38022  lhp0lt  38024  lhpexle2lem  38030  lhpexle3lem  38032  lhpjat2  38042  lhpj1  38043  lhpmcvr3  38046  lhpmcvr4N  38047  lhpmcvr5N  38048  lhpmcvr6N  38049  lhpmatb  38052  lhp2at0  38053  lhp2atnle  38054  lhp2at0nle  38056  lhprelat3N  38061  lhple  38063  lhpat4N  38065  lhpat3  38067  4atexlemtlw  38088  4atexlemc  38090  4atexlemnclw  38091  4atexlemcnd  38093  4atex2-0aOLDN  38099  lauteq  38116  ltrnid  38156  ltrnel  38160  ltrnat  38161  ltrncnvat  38162  ltrncnvel  38163  ltrncoval  38166  ltrncnv  38167  ltrn11at  38168  ltrneq2  38169  ltrneq  38170  idltrn  38171  trlval2  38184  trlcnv  38186  trljat1  38187  trljat2  38188  ltrnideq  38196  arglem1N  38211  cdlemc1  38212  cdlemc2  38213  cdlemc4  38215  cdlemc5  38216  cdlemc6  38217  cdlemd1  38219  cdlemd2  38220  cdlemd3  38221  cdlemd4  38222  cdlemd7  38225  cdleme0aa  38231  cdleme0b  38233  cdleme0c  38234  cdleme0cp  38235  cdleme0cq  38236  cdleme0e  38238  cdleme0fN  38239  cdleme1b  38247  cdleme1  38248  cdleme2  38249  cdleme3b  38250  cdleme3c  38251  cdleme3e  38253  cdleme3g  38255  cdleme3h  38256  cdleme3  38258  cdleme5  38261  cdleme7d  38267  cdleme7e  38268  cdleme7ga  38269  cdleme7  38270  cdleme8  38271  cdleme9  38274  cdleme10  38275  cdleme11c  38282  cdleme11e  38284  cdleme11fN  38285  cdleme11g  38286  cdleme11k  38289  cdleme11  38291  cdleme15b  38296  cdleme15  38299  cdleme16b  38300  cdleme17b  38308  cdleme17c  38309  cdlemednpq  38320  cdleme20zN  38322  cdleme19a  38324  cdleme20bN  38331  cdleme20d  38333  cdleme20j  38339  cdleme21c  38348  cdleme22aa  38360  cdleme22b  38362  cdleme22cN  38363  cdleme22d  38364  cdleme22e  38365  cdleme22eALTN  38366  cdleme23b  38371  cdleme23c  38372  cdleme27N  38390  cdleme28a  38391  cdleme30a  38399  cdlemefrs29pre00  38416  cdlemefrs29bpre0  38417  cdlemefrs29cpre1  38419  cdlemefrs32fva  38421  cdlemefrs32fva1  38422  cdlemefr32snb  38426  cdlemefs32snb  38436  cdleme32snb  38457  cdleme32fva  38458  cdleme32fva1  38459  cdleme32fvaw  38460  cdleme35a  38469  cdleme35fnpq  38470  cdleme35b  38471  cdleme35c  38472  cdleme35f  38475  cdleme42c  38493  cdleme42e  38500  cdleme42h  38503  cdleme42i  38504  cdleme42ke  38506  cdleme42keg  38507  cdleme42mgN  38509  cdleme17d4  38518  cdleme48fvg  38521  cdleme48bw  38523  cdlemeg46req  38550  cdleme50trn3  38574  cdlemf1  38582  cdlemf2  38583  trlord  38590  ltrniotacnvval  38603  cdlemg2fv2  38621  cdlemg2l  38624  cdlemg7fvbwN  38628  cdlemg4c  38633  cdlemg4  38638  cdlemg6c  38641  cdlemg8b  38649  cdlemg11b  38663  cdlemg13a  38672  cdlemg17a  38682  cdlemg17h  38689  cdlemg17  38698  cdlemg18b  38700  cdlemg19a  38704  cdlemg27a  38713  cdlemg27b  38717  cdlemg31a  38718  cdlemg31b  38719  cdlemg31d  38721  cdlemg33b0  38722  cdlemg33a  38727  cdlemg35  38734  trlcolem  38747  cdlemg42  38750  cdlemg44a  38752  cdlemg46  38756  cdlemh1  38836  cdlemh2  38837  cdlemh  38838  cdlemi1  38839  cdlemi  38841  cdlemk3  38854  cdlemk4  38855  cdlemkvcl  38863  cdlemk7  38869  cdlemk11  38870  cdlemk15  38876  cdlemk1u  38880  cdlemk7u  38891  cdlemk11u  38892  cdlemk37  38935  cdlemk39  38937  cdlemkid1  38943  cdlemkid2  38945  cdlemk48  38971  cdlemk50  38973  cdlemk51  38974  cdlemk52  38975  dia2dimlem1  39085  dia2dimlem2  39086  dia2dimlem3  39087  dia2dimlem5  39089  dia2dimlem7  39091  dia2dimlem9  39093  dia2dimlem10  39094  dia2dimlem12  39096  dia2dimlem13  39097  cdlemm10N  39139  cdlemn2  39216  cdlemn3  39218  cdlemn9  39226  cdlemn10  39227  dihjustlem  39237  dihord1  39239  dihord2pre2  39247  dihvalcqat  39260  dib2dim  39264  dih2dimb  39265  dih2dimbALTN  39266  dihord5apre  39283  dihglbcpreN  39321  dihmeetlem3N  39326  dihmeetlem6  39330  dihjatc1  39332  dihjatc2N  39333  dihjatc3  39334  dihmeetlem9N  39336  dihmeetlem10N  39337  dihmeetlem11N  39338  dihmeetlem13N  39340  dihmeetlem15N  39342  dihmeetlem16N  39343  dihmeetlem17N  39344  dihatexv2  39360  dihjatb  39437  dihjatc  39438  dihjatcclem1  39439  dihjatcclem2  39440  dihjatcclem4  39442  dihjat  39444  dihjat3  39453  dihjat5N  39458  dvh4dimat  39459