Theorem atbase 38462

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  Vcvv 3472  ∅c0 4321   class class class wbr 5147  ‘cfv 6542  Basecbs 17148  0.cp0 18380   ⋖ ccvr 38435  Atomscatm 38436

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-iota 6494  df-fun 6544  df-fv 6550  df-ats 38440

This theorem is referenced by:  atssbase  38463  0ltat  38464  leatb  38465  meetat  38469  atnle0  38482  atlen0  38483  atcmp  38484  atcvreq0  38487  atncvrN  38488  atnle  38490  atnem0  38491  atlatmstc  38492  atlatle  38493  cvlexch2  38502  cvlexchb1  38503  cvlexchb2  38504  cvlatexchb1  38507  cvlatexchb2  38508  cvlatexch1  38509  cvlatexch2  38510  cvlatexch3  38511  cvlcvr1  38512  cvlcvrp  38513  cvlatcvr1  38514  cvlatcvr2  38515  cvlsupr2  38516  cvlsupr7  38521  cvlsupr8  38522  hlatjcl  38540  hlatjcom  38541  hlatjidm  38542  hlatjass  38543  hlatj32  38545  hlatj4  38547  hlatlej1  38548  atnlej1  38553  atnlej2  38554  hlrelat5N  38575  hlrelat  38576  hlrelat2  38577  exatleN  38578  cvr2N  38585  hlrelat3  38586  cvrval3  38587  cvrval5  38589  cvrexchlem  38593  cvratlem  38595  cvrat  38596  atcvr0eq  38600  lnnat  38601  cvrat2  38603  atcvrneN  38604  atcvrj1  38605  atcvrj2b  38606  atltcvr  38609  atle  38610  atlelt  38612  2atlt  38613  atexchcvrN  38614  cvrat3  38616  cvrat4  38617  cvrat42  38618  2atjm  38619  atbtwn  38620  3noncolr2  38623  4noncolr3  38627  athgt  38630  3dim0  38631  3dimlem3a  38634  3dimlem3OLDN  38636  3dimlem4a  38637  3dimlem4OLDN  38639  3dim3  38643  2dim  38644  1cvratex  38647  1cvrjat  38649  1cvrat  38650  ps-1  38651  ps-2  38652  hlatexch3N  38654  hlatexch4  38655  ps-2b  38656  3atlem1  38657  3atlem2  38658  3atlem4  38660  3atlem5  38661  3atlem6  38662  3at  38664  islln3  38684  llnnleat  38687  llnn0  38690  llnle  38692  llnexatN  38695  llncmp  38696  2llnmat  38698  2at0mat0  38699  2atm  38701  ps-2c  38702  lplni2  38711  lplnle  38714  lplnnle2at  38715  lplnn0N  38721  islpln2a  38722  2atmat  38735  lplnexllnN  38738  2llnjaN  38740  2llnm4  38744  2llnmeqat  38745  lvoli3  38751  islvol5  38753  lvoli2  38755  lvolnle3at  38756  3atnelvolN  38760  lvoln0N  38765  islvol2aN  38766  4atlem3  38770  4atlem3a  38771  4atlem3b  38772  4atlem4a  38773  4atlem4b  38774  4atlem4c  38775  4atlem4d  38776  4atlem9  38777  4atlem10a  38778  4atlem10  38780  4atlem11a  38781  4atlem11b  38782  4atlem11  38783  4atlem12a  38784  4atlem12b  38785  4atlem12  38786  4at2  38788  lplncvrlvol2  38789  2lplnja  38793  dalempeb  38813  dalemqeb  38814  dalemreb  38815  dalemseb  38816  dalemteb  38817  dalemueb  38818  dalem3  38838  dalem16  38853  dalemcceb  38863  dalem21  38868  dalem25  38872  dalem38  38884  dalem39  38885  dalem43  38889  dalem44  38890  dalem45  38891  dalem53  38899  dalem54  38900  dalem55  38901  dalem57  38903  dalem60  38906  snatpsubN  38924  linepsubN  38926  pmaple  38935  pmapat  38937  pmap1N  38941  pmapsub  38942  pmapglbx  38943  isline2  38948  linepmap  38949  isline3  38950  isline4N  38951  lneq2at  38952  lncvrelatN  38955  lncmp  38957  2lnat  38958  2atm2atN  38959  2llnma1b  38960  2llnma1  38961  2llnma3r  38962  cdlema1N  38965  cdlemblem  38967  cdlemb  38968  elpaddn0  38974  paddcom  38987  paddasslem2  38995  paddasslem5  38998  paddasslem12  39005  paddasslem13  39006  pmapjoin  39026  pmapjat1  39027  pmapjat2  39028  pmapjlln1  39029  atmod1i1  39031  atmod1i2  39033  llnmod1i2  39034  atmod2i1  39035  atmod2i2  39036  atmod3i1  39038  atmod3i2  39039  atmod4i1  39040  atmod4i2  39041  llnexchb2lem  39042  llnexchb2  39043  dalawlem2  39046  dalawlem3  39047  dalawlem5  39049  dalawlem6  39050  dalawlem7  39051  dalawlem8  39052  dalawlem11  39055  dalawlem12  39056  polval2N  39080  pol1N  39084  polatN  39105  2polatN  39106  paddatclN  39123  linepsubclN  39125  lhp2lt  39175  lhp0lt  39177  lhpexle2lem  39183  lhpexle3lem  39185  lhpjat2  39195  lhpj1  39196  lhpmcvr3  39199  lhpmcvr4N  39200  lhpmcvr5N  39201  lhpmcvr6N  39202  lhpmatb  39205  lhp2at0  39206  lhp2atnle  39207  lhp2at0nle  39209  lhprelat3N  39214  lhple  39216  lhpat4N  39218  lhpat3  39220  4atexlemtlw  39241  4atexlemc  39243  4atexlemnclw  39244  4atexlemcnd  39246  4atex2-0aOLDN  39252  lauteq  39269  ltrnid  39309  ltrnel  39313  ltrnat  39314  ltrncnvat  39315  ltrncnvel  39316  ltrncoval  39319  ltrncnv  39320  ltrn11at  39321  ltrneq2  39322  ltrneq  39323  idltrn  39324  trlval2  39337  trlcnv  39339  trljat1  39340  trljat2  39341  ltrnideq  39349  arglem1N  39364  cdlemc1  39365  cdlemc2  39366  cdlemc4  39368  cdlemc5  39369  cdlemc6  39370  cdlemd1  39372  cdlemd2  39373  cdlemd3  39374  cdlemd4  39375  cdlemd7  39378  cdleme0aa  39384  cdleme0b  39386  cdleme0c  39387  cdleme0cp  39388  cdleme0cq  39389  cdleme0e  39391  cdleme0fN  39392  cdleme1b  39400  cdleme1  39401  cdleme2  39402  cdleme3b  39403  cdleme3c  39404  cdleme3e  39406  cdleme3g  39408  cdleme3h  39409  cdleme3  39411  cdleme5  39414  cdleme7d  39420  cdleme7e  39421  cdleme7ga  39422  cdleme7  39423  cdleme8  39424  cdleme9  39427  cdleme10  39428  cdleme11c  39435  cdleme11e  39437  cdleme11fN  39438  cdleme11g  39439  cdleme11k  39442  cdleme11  39444  cdleme15b  39449  cdleme15  39452  cdleme16b  39453  cdleme17b  39461  cdleme17c  39462  cdlemednpq  39473  cdleme20zN  39475  cdleme19a  39477  cdleme20bN  39484  cdleme20d  39486  cdleme20j  39492  cdleme21c  39501  cdleme22aa  39513  cdleme22b  39515  cdleme22cN  39516  cdleme22d  39517  cdleme22e  39518  cdleme22eALTN  39519  cdleme23b  39524  cdleme23c  39525  cdleme27N  39543  cdleme28a  39544  cdleme30a  39552  cdlemefrs29pre00  39569  cdlemefrs29bpre0  39570  cdlemefrs29cpre1  39572  cdlemefrs32fva  39574  cdlemefrs32fva1  39575  cdlemefr32snb  39579  cdlemefs32snb  39589  cdleme32snb  39610  cdleme32fva  39611  cdleme32fva1  39612  cdleme32fvaw  39613  cdleme35a  39622  cdleme35fnpq  39623  cdleme35b  39624  cdleme35c  39625  cdleme35f  39628  cdleme42c  39646  cdleme42e  39653  cdleme42h  39656  cdleme42i  39657  cdleme42ke  39659  cdleme42keg  39660  cdleme42mgN  39662  cdleme17d4  39671  cdleme48fvg  39674  cdleme48bw  39676  cdlemeg46req  39703  cdleme50trn3  39727  cdlemf1  39735  cdlemf2  39736  trlord  39743  ltrniotacnvval  39756  cdlemg2fv2  39774  cdlemg2l  39777  cdlemg7fvbwN  39781  cdlemg4c  39786  cdlemg4  39791  cdlemg6c  39794  cdlemg8b  39802  cdlemg11b  39816  cdlemg13a  39825  cdlemg17a  39835  cdlemg17h  39842  cdlemg17  39851  cdlemg18b  39853  cdlemg19a  39857  cdlemg27a  39866  cdlemg27b  39870  cdlemg31a  39871  cdlemg31b  39872  cdlemg31d  39874  cdlemg33b0  39875  cdlemg33a  39880  cdlemg35  39887  trlcolem  39900  cdlemg42  39903  cdlemg44a  39905  cdlemg46  39909  cdlemh1  39989  cdlemh2  39990  cdlemh  39991  cdlemi1  39992  cdlemi  39994  cdlemk3  40007  cdlemk4  40008  cdlemkvcl  40016  cdlemk7  40022  cdlemk11  40023  cdlemk15  40029  cdlemk1u  40033  cdlemk7u  40044  cdlemk11u  40045  cdlemk37  40088  cdlemk39  40090  cdlemkid1  40096  cdlemkid2  40098  cdlemk48  40124  cdlemk50  40126  cdlemk51  40127  cdlemk52  40128  dia2dimlem1  40238  dia2dimlem2  40239  dia2dimlem3  40240  dia2dimlem5  40242  dia2dimlem7  40244  dia2dimlem9  40246  dia2dimlem10  40247  dia2dimlem12  40249  dia2dimlem13  40250  cdlemm10N  40292  cdlemn2  40369  cdlemn3  40371  cdlemn9  40379  cdlemn10  40380  dihjustlem  40390  dihord1  40392  dihord2pre2  40400  dihvalcqat  40413  dib2dim  40417  dih2dimb  40418  dih2dimbALTN  40419  dihord5apre  40436  dihglbcpreN  40474  dihmeetlem3N  40479  dihmeetlem6  40483  dihjatc1  40485  dihjatc2N  40486  dihjatc3  40487  dihmeetlem9N  40489  dihmeetlem10N  40490  dihmeetlem11N  40491  dihmeetlem13N  40493  dihmeetlem15N  40495  dihmeetlem16N  40496  dihmeetlem17N  40497  dihatexv2  40513  dihjatb  40590  dihjatc  40591  dihjatcclem1  40592  dihjatcclem2  40593  dihjatcclem4  40595  dihjat  40597  dihjat3  40606  dihjat5N  40611  dvh4dimat  40612