Theorem atbase 35069

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 29531 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 4121	. . . 4 ⊢ (𝑃 ∈ 𝐴 → ¬ 𝐴 = ∅)
2		atombase.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
3	2	eqeq1i 2811	. . . 4 ⊢ (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
4	1, 3	sylnib 319	. . 3 ⊢ (𝑃 ∈ 𝐴 → ¬ (Atoms‘𝐾) = ∅)
5		fvprc 6401	. . 3 ⊢ (¬ 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
6	4, 5	nsyl2 144	. 2 ⊢ (𝑃 ∈ 𝐴 → 𝐾 ∈ V)
7		atombase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2806	. . . 4 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		eqid 2806	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	isat 35066	. . 3 ⊢ (𝐾 ∈ V → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
11	10	simprbda 488	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐵)
12	6, 11	mpancom 671	1 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1637   ∈ wcel 2156  Vcvv 3391  ∅c0 4116   class class class wbr 4844  ‘cfv 6101  Basecbs 16068  0.cp0 17242   ⋖ ccvr 35042  Atomscatm 35043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-iota 6064  df-fun 6103  df-fv 6109  df-ats 35047

This theorem is referenced by:  atssbase  35070  0ltat  35071  leatb  35072  meetat  35076  atnle0  35089  atlen0  35090  atcmp  35091  atcvreq0  35094  atncvrN  35095  atnle  35097  atnem0  35098  atlatmstc  35099  atlatle  35100  cvlexch2  35109  cvlexchb1  35110  cvlexchb2  35111  cvlatexchb1  35114  cvlatexchb2  35115  cvlatexch1  35116  cvlatexch2  35117  cvlatexch3  35118  cvlcvr1  35119  cvlcvrp  35120  cvlatcvr1  35121  cvlatcvr2  35122  cvlsupr2  35123  cvlsupr7  35128  cvlsupr8  35129  hlatjcl  35147  hlatjcom  35148  hlatjidm  35149  hlatjass  35150  hlatj32  35152  hlatj4  35154  hlatlej1  35155  atnlej1  35159  atnlej2  35160  hlrelat5N  35181  hlrelat  35182  hlrelat2  35183  exatleN  35184  cvr2N  35191  hlrelat3  35192  cvrval3  35193  cvrval5  35195  cvrexchlem  35199  cvratlem  35201  cvrat  35202  atcvr0eq  35206  lnnat  35207  cvrat2  35209  atcvrneN  35210  atcvrj1  35211  atcvrj2b  35212  atltcvr  35215  atle  35216  atlelt  35218  2atlt  35219  atexchcvrN  35220  cvrat3  35222  cvrat4  35223  cvrat42  35224  2atjm  35225  atbtwn  35226  3noncolr2  35229  4noncolr3  35233  athgt  35236  3dim0  35237  3dimlem3a  35240  3dimlem3OLDN  35242  3dimlem4a  35243  3dimlem4OLDN  35245  3dim3  35249  2dim  35250  1cvratex  35253  1cvrjat  35255  1cvrat  35256  ps-1  35257  ps-2  35258  hlatexch3N  35260  hlatexch4  35261  ps-2b  35262  3atlem1  35263  3atlem2  35264  3atlem4  35266  3atlem5  35267  3atlem6  35268  3at  35270  islln3  35290  llnnleat  35293  llnn0  35296  llnle  35298  llnexatN  35301  llncmp  35302  2llnmat  35304  2at0mat0  35305  2atm  35307  ps-2c  35308  lplni2  35317  lplnle  35320  lplnnle2at  35321  lplnn0N  35327  islpln2a  35328  2atmat  35341  lplnexllnN  35344  2llnjaN  35346  2llnm4  35350  2llnmeqat  35351  lvoli3  35357  islvol5  35359  lvoli2  35361  lvolnle3at  35362  3atnelvolN  35366  lvoln0N  35371  islvol2aN  35372  4atlem3  35376  4atlem3a  35377  4atlem3b  35378  4atlem4a  35379  4atlem4b  35380  4atlem4c  35381  4atlem4d  35382  4atlem9  35383  4atlem10a  35384  4atlem10  35386  4atlem11a  35387  4atlem11b  35388  4atlem11  35389  4atlem12a  35390  4atlem12b  35391  4atlem12  35392  4at2  35394  lplncvrlvol2  35395  2lplnja  35399  dalempeb  35419  dalemqeb  35420  dalemreb  35421  dalemseb  35422  dalemteb  35423  dalemueb  35424  dalem3  35444  dalem16  35459  dalemcceb  35469  dalem21  35474  dalem25  35478  dalem38  35490  dalem39  35491  dalem43  35495  dalem44  35496  dalem45  35497  dalem53  35505  dalem54  35506  dalem55  35507  dalem57  35509  dalem60  35512  snatpsubN  35530  linepsubN  35532  pmaple  35541  pmapat  35543  pmap1N  35547  pmapsub  35548  pmapglbx  35549  isline2  35554  linepmap  35555  isline3  35556  isline4N  35557  lneq2at  35558  lncvrelatN  35561  lncmp  35563  2lnat  35564  2atm2atN  35565  2llnma1b  35566  2llnma1  35567  2llnma3r  35568  cdlema1N  35571  cdlemblem  35573  cdlemb  35574  elpaddn0  35580  paddcom  35593  paddasslem2  35601  paddasslem5  35604  paddasslem12  35611  paddasslem13  35612  pmapjoin  35632  pmapjat1  35633  pmapjat2  35634  pmapjlln1  35635  atmod1i1  35637  atmod1i2  35639  llnmod1i2  35640  atmod2i1  35641  atmod2i2  35642  atmod3i1  35644  atmod3i2  35645  atmod4i1  35646  atmod4i2  35647  llnexchb2lem  35648  llnexchb2  35649  dalawlem2  35652  dalawlem3  35653  dalawlem5  35655  dalawlem6  35656  dalawlem7  35657  dalawlem8  35658  dalawlem11  35661  dalawlem12  35662  polval2N  35686  pol1N  35690  polatN  35711  2polatN  35712  paddatclN  35729  linepsubclN  35731  lhp2lt  35781  lhp0lt  35783  lhpexle2lem  35789  lhpexle3lem  35791  lhpjat2  35801  lhpj1  35802  lhpmcvr3  35805  lhpmcvr4N  35806  lhpmcvr5N  35807  lhpmcvr6N  35808  lhpmatb  35811  lhp2at0  35812  lhp2atnle  35813  lhp2at0nle  35815  lhprelat3N  35820  lhple  35822  lhpat4N  35824  lhpat3  35826  4atexlemtlw  35847  4atexlemc  35849  4atexlemnclw  35850  4atexlemcnd  35852  4atex2-0aOLDN  35858  lauteq  35875  ltrnid  35915  ltrnel  35919  ltrnat  35920  ltrncnvat  35921  ltrncnvel  35922  ltrncoval  35925  ltrncnv  35926  ltrn11at  35927  ltrneq2  35928  ltrneq  35929  idltrn  35930  ltrnmwOLD  35932  trlval2  35944  trlcnv  35946  trljat1  35947  trljat2  35948  ltrnideq  35956  arglem1N  35971  cdlemc1  35972  cdlemc2  35973  cdlemc4  35975  cdlemc5  35976  cdlemc6  35977  cdlemd1  35979  cdlemd2  35980  cdlemd3  35981  cdlemd4  35982  cdlemd7  35985  cdleme0aa  35991  cdleme0b  35993  cdleme0c  35994  cdleme0cp  35995  cdleme0cq  35996  cdleme0e  35998  cdleme0fN  35999  cdleme1b  36007  cdleme1  36008  cdleme2  36009  cdleme3b  36010  cdleme3c  36011  cdleme3e  36013  cdleme3g  36015  cdleme3h  36016  cdleme3  36018  cdleme5  36021  cdleme7d  36027  cdleme7e  36028  cdleme7ga  36029  cdleme7  36030  cdleme8  36031  cdleme9  36034  cdleme10  36035  cdleme11c  36042  cdleme11e  36044  cdleme11fN  36045  cdleme11g  36046  cdleme11k  36049  cdleme11  36051  cdleme15b  36056  cdleme15  36059  cdleme16b  36060  cdleme17b  36068  cdleme17c  36069  cdlemednpq  36080  cdleme20zN  36082  cdleme19a  36084  cdleme20bN  36091  cdleme20d  36093  cdleme20j  36099  cdleme21c  36108  cdleme22aa  36120  cdleme22b  36122  cdleme22cN  36123  cdleme22d  36124  cdleme22e  36125  cdleme22eALTN  36126  cdleme23b  36131  cdleme23c  36132  cdleme27N  36150  cdleme28a  36151  cdleme30a  36159  cdlemefrs29pre00  36176  cdlemefrs29bpre0  36177  cdlemefrs29cpre1  36179  cdlemefrs32fva  36181  cdlemefrs32fva1  36182  cdlemefr32snb  36186  cdlemefs32snb  36196  cdleme32snb  36217  cdleme32fva  36218  cdleme32fva1  36219  cdleme32fvaw  36220  cdleme35a  36229  cdleme35fnpq  36230  cdleme35b  36231  cdleme35c  36232  cdleme35f  36235  cdleme42c  36253  cdleme42e  36260  cdleme42h  36263  cdleme42i  36264  cdleme42ke  36266  cdleme42keg  36267  cdleme42mgN  36269  cdleme17d4  36278  cdleme48fvg  36281  cdleme48bw  36283  cdlemeg46req  36310  cdleme50trn3  36334  cdlemf1  36342  cdlemf2  36343  trlord  36350  ltrniotacnvval  36363  cdlemg2fv2  36381  cdlemg2l  36384  cdlemg7fvbwN  36388  cdlemg4c  36393  cdlemg4  36398  cdlemg6c  36401  cdlemg8b  36409  cdlemg11b  36423  cdlemg13a  36432  cdlemg17a  36442  cdlemg17h  36449  cdlemg17  36458  cdlemg18b  36460  cdlemg19a  36464  cdlemg27a  36473  cdlemg27b  36477  cdlemg31a  36478  cdlemg31b  36479  cdlemg31d  36481  cdlemg33b0  36482  cdlemg33a  36487  cdlemg35  36494  trlcolem  36507  cdlemg42  36510  cdlemg44a  36512  cdlemg46  36516  cdlemh1  36596  cdlemh2  36597  cdlemh  36598  cdlemi1  36599  cdlemi  36601  cdlemk3  36614  cdlemk4  36615  cdlemkvcl  36623  cdlemk7  36629  cdlemk11  36630  cdlemk15  36636  cdlemk1u  36640  cdlemk7u  36651  cdlemk11u  36652  cdlemk37  36695  cdlemk39  36697  cdlemkid1  36703  cdlemkid2  36705  cdlemk48  36731  cdlemk50  36733  cdlemk51  36734  cdlemk52  36735  dia2dimlem1  36845  dia2dimlem2  36846  dia2dimlem3  36847  dia2dimlem5  36849  dia2dimlem7  36851  dia2dimlem9  36853  dia2dimlem10  36854  dia2dimlem12  36856  dia2dimlem13  36857  cdlemm10N  36899  cdlemn2  36976  cdlemn3  36978  cdlemn9  36986  cdlemn10  36987  dihjustlem  36997  dihord1  36999  dihord2pre2  37007  dihvalcqat  37020  dib2dim  37024  dih2dimb  37025  dih2dimbALTN  37026  dihord5apre  37043  dihglbcpreN  37081  dihmeetlem3N  37086  dihmeetlem6  37090  dihjatc1  37092  dihjatc2N  37093  dihjatc3  37094  dihmeetlem9N  37096  dihmeetlem10N  37097  dihmeetlem11N  37098  dihmeetlem13N  37100  dihmeetlem15N  37102  dihmeetlem16N  37103  dihmeetlem17N  37104  dihatexv2  37120  dihjatb  37197  dihjatc  37198  dihjatcclem1  37199  dihjatcclem2  37200  dihjatcclem4  37202  dihjat  37204  dihjat3  37213  dihjat5N  37218  dvh4dimat  37219