Theorem atbase 39327

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  Vcvv 3436  ∅c0 4283   class class class wbr 5091  ‘cfv 6481  Basecbs 17117  0.cp0 18324   ⋖ ccvr 39300  Atomscatm 39301

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-iota 6437  df-fun 6483  df-fv 6489  df-ats 39305

This theorem is referenced by:  atssbase  39328  0ltat  39329  leatb  39330  meetat  39334  atnle0  39347  atlen0  39348  atcmp  39349  atcvreq0  39352  atncvrN  39353  atnle  39355  atnem0  39356  atlatmstc  39357  atlatle  39358  cvlexch2  39367  cvlexchb1  39368  cvlexchb2  39369  cvlatexchb1  39372  cvlatexchb2  39373  cvlatexch1  39374  cvlatexch2  39375  cvlatexch3  39376  cvlcvr1  39377  cvlcvrp  39378  cvlatcvr1  39379  cvlatcvr2  39380  cvlsupr2  39381  cvlsupr7  39386  cvlsupr8  39387  hlatjcl  39405  hlatjcom  39406  hlatjidm  39407  hlatjass  39408  hlatj32  39410  hlatj4  39412  hlatlej1  39413  atnlej1  39417  atnlej2  39418  hlrelat5N  39439  hlrelat  39440  hlrelat2  39441  exatleN  39442  cvr2N  39449  hlrelat3  39450  cvrval3  39451  cvrval5  39453  cvrexchlem  39457  cvratlem  39459  cvrat  39460  atcvr0eq  39464  lnnat  39465  cvrat2  39467  atcvrneN  39468  atcvrj1  39469  atcvrj2b  39470  atltcvr  39473  atle  39474  atlelt  39476  2atlt  39477  atexchcvrN  39478  cvrat3  39480  cvrat4  39481  cvrat42  39482  2atjm  39483  atbtwn  39484  3noncolr2  39487  4noncolr3  39491  athgt  39494  3dim0  39495  3dimlem3a  39498  3dimlem3OLDN  39500  3dimlem4a  39501  3dimlem4OLDN  39503  3dim3  39507  2dim  39508  1cvratex  39511  1cvrjat  39513  1cvrat  39514  ps-1  39515  ps-2  39516  hlatexch3N  39518  hlatexch4  39519  ps-2b  39520  3atlem1  39521  3atlem2  39522  3atlem4  39524  3atlem5  39525  3atlem6  39526  3at  39528  islln3  39548  llnnleat  39551  llnn0  39554  llnle  39556  llnexatN  39559  llncmp  39560  2llnmat  39562  2at0mat0  39563  2atm  39565  ps-2c  39566  lplni2  39575  lplnle  39578  lplnnle2at  39579  lplnn0N  39585  islpln2a  39586  2atmat  39599  lplnexllnN  39602  2llnjaN  39604  2llnm4  39608  2llnmeqat  39609  lvoli3  39615  islvol5  39617  lvoli2  39619  lvolnle3at  39620  3atnelvolN  39624  lvoln0N  39629  islvol2aN  39630  4atlem3  39634  4atlem3a  39635  4atlem3b  39636  4atlem4a  39637  4atlem4b  39638  4atlem4c  39639  4atlem4d  39640  4atlem9  39641  4atlem10a  39642  4atlem10  39644  4atlem11a  39645  4atlem11b  39646  4atlem11  39647  4atlem12a  39648  4atlem12b  39649  4atlem12  39650  4at2  39652  lplncvrlvol2  39653  2lplnja  39657  dalempeb  39677  dalemqeb  39678  dalemreb  39679  dalemseb  39680  dalemteb  39681  dalemueb  39682  dalem3  39702  dalem16  39717  dalemcceb  39727  dalem21  39732  dalem25  39736  dalem38  39748  dalem39  39749  dalem43  39753  dalem44  39754  dalem45  39755  dalem53  39763  dalem54  39764  dalem55  39765  dalem57  39767  dalem60  39770  snatpsubN  39788  linepsubN  39790  pmaple  39799  pmapat  39801  pmap1N  39805  pmapsub  39806  pmapglbx  39807  isline2  39812  linepmap  39813  isline3  39814  isline4N  39815  lneq2at  39816  lncvrelatN  39819  lncmp  39821  2lnat  39822  2atm2atN  39823  2llnma1b  39824  2llnma1  39825  2llnma3r  39826  cdlema1N  39829  cdlemblem  39831  cdlemb  39832  elpaddn0  39838  paddcom  39851  paddasslem2  39859  paddasslem5  39862  paddasslem12  39869  paddasslem13  39870  pmapjoin  39890  pmapjat1  39891  pmapjat2  39892  pmapjlln1  39893  atmod1i1  39895  atmod1i2  39897  llnmod1i2  39898  atmod2i1  39899  atmod2i2  39900  atmod3i1  39902  atmod3i2  39903  atmod4i1  39904  atmod4i2  39905  llnexchb2lem  39906  llnexchb2  39907  dalawlem2  39910  dalawlem3  39911  dalawlem5  39913  dalawlem6  39914  dalawlem7  39915  dalawlem8  39916  dalawlem11  39919  dalawlem12  39920  polval2N  39944  pol1N  39948  polatN  39969  2polatN  39970  paddatclN  39987  linepsubclN  39989  lhp2lt  40039  lhp0lt  40041  lhpexle2lem  40047  lhpexle3lem  40049  lhpjat2  40059  lhpj1  40060  lhpmcvr3  40063  lhpmcvr4N  40064  lhpmcvr5N  40065  lhpmcvr6N  40066  lhpmatb  40069  lhp2at0  40070  lhp2atnle  40071  lhp2at0nle  40073  lhprelat3N  40078  lhple  40080  lhpat4N  40082  lhpat3  40084  4atexlemtlw  40105  4atexlemc  40107  4atexlemnclw  40108  4atexlemcnd  40110  4atex2-0aOLDN  40116  lauteq  40133  ltrnid  40173  ltrnel  40177  ltrnat  40178  ltrncnvat  40179  ltrncnvel  40180  ltrncoval  40183  ltrncnv  40184  ltrn11at  40185  ltrneq2  40186  ltrneq  40187  idltrn  40188  trlval2  40201  trlcnv  40203  trljat1  40204  trljat2  40205  ltrnideq  40213  arglem1N  40228  cdlemc1  40229  cdlemc2  40230  cdlemc4  40232  cdlemc5  40233  cdlemc6  40234  cdlemd1  40236  cdlemd2  40237  cdlemd3  40238  cdlemd4  40239  cdlemd7  40242  cdleme0aa  40248  cdleme0b  40250  cdleme0c  40251  cdleme0cp  40252  cdleme0cq  40253  cdleme0e  40255  cdleme0fN  40256  cdleme1b  40264  cdleme1  40265  cdleme2  40266  cdleme3b  40267  cdleme3c  40268  cdleme3e  40270  cdleme3g  40272  cdleme3h  40273  cdleme3  40275  cdleme5  40278  cdleme7d  40284  cdleme7e  40285  cdleme7ga  40286  cdleme7  40287  cdleme8  40288  cdleme9  40291  cdleme10  40292  cdleme11c  40299  cdleme11e  40301  cdleme11fN  40302  cdleme11g  40303  cdleme11k  40306  cdleme11  40308  cdleme15b  40313  cdleme15  40316  cdleme16b  40317  cdleme17b  40325  cdleme17c  40326  cdlemednpq  40337  cdleme20zN  40339  cdleme19a  40341  cdleme20bN  40348  cdleme20d  40350  cdleme20j  40356  cdleme21c  40365  cdleme22aa  40377  cdleme22b  40379  cdleme22cN  40380  cdleme22d  40381  cdleme22e  40382  cdleme22eALTN  40383  cdleme23b  40388  cdleme23c  40389  cdleme27N  40407  cdleme28a  40408  cdleme30a  40416  cdlemefrs29pre00  40433  cdlemefrs29bpre0  40434  cdlemefrs29cpre1  40436  cdlemefrs32fva  40438  cdlemefrs32fva1  40439  cdlemefr32snb  40443  cdlemefs32snb  40453  cdleme32snb  40474  cdleme32fva  40475  cdleme32fva1  40476  cdleme32fvaw  40477  cdleme35a  40486  cdleme35fnpq  40487  cdleme35b  40488  cdleme35c  40489  cdleme35f  40492  cdleme42c  40510  cdleme42e  40517  cdleme42h  40520  cdleme42i  40521  cdleme42ke  40523  cdleme42keg  40524  cdleme42mgN  40526  cdleme17d4  40535  cdleme48fvg  40538  cdleme48bw  40540  cdlemeg46req  40567  cdleme50trn3  40591  cdlemf1  40599  cdlemf2  40600  trlord  40607  ltrniotacnvval  40620  cdlemg2fv2  40638  cdlemg2l  40641  cdlemg7fvbwN  40645  cdlemg4c  40650  cdlemg4  40655  cdlemg6c  40658  cdlemg8b  40666  cdlemg11b  40680  cdlemg13a  40689  cdlemg17a  40699  cdlemg17h  40706  cdlemg17  40715  cdlemg18b  40717  cdlemg19a  40721  cdlemg27a  40730  cdlemg27b  40734  cdlemg31a  40735  cdlemg31b  40736  cdlemg31d  40738  cdlemg33b0  40739  cdlemg33a  40744  cdlemg35  40751  trlcolem  40764  cdlemg42  40767  cdlemg44a  40769  cdlemg46  40773  cdlemh1  40853  cdlemh2  40854  cdlemh  40855  cdlemi1  40856  cdlemi  40858  cdlemk3  40871  cdlemk4  40872  cdlemkvcl  40880  cdlemk7  40886  cdlemk11  40887  cdlemk15  40893  cdlemk1u  40897  cdlemk7u  40908  cdlemk11u  40909  cdlemk37  40952  cdlemk39  40954  cdlemkid1  40960  cdlemkid2  40962  cdlemk48  40988  cdlemk50  40990  cdlemk51  40991  cdlemk52  40992  dia2dimlem1  41102  dia2dimlem2  41103  dia2dimlem3  41104  dia2dimlem5  41106  dia2dimlem7  41108  dia2dimlem9  41110  dia2dimlem10  41111  dia2dimlem12  41113  dia2dimlem13  41114  cdlemm10N  41156  cdlemn2  41233  cdlemn3  41235  cdlemn9  41243  cdlemn10  41244  dihjustlem  41254  dihord1  41256  dihord2pre2  41264  dihvalcqat  41277  dib2dim  41281  dih2dimb  41282  dih2dimbALTN  41283  dihord5apre  41300  dihglbcpreN  41338  dihmeetlem3N  41343  dihmeetlem6  41347  dihjatc1  41349  dihjatc2N  41350  dihjatc3  41351  dihmeetlem9N  41353  dihmeetlem10N  41354  dihmeetlem11N  41355  dihmeetlem13N  41357  dihmeetlem15N  41359  dihmeetlem16N  41360  dihmeetlem17N  41361  dihatexv2  41377  dihjatb  41454  dihjatc  41455  dihjatcclem1  41456  dihjatcclem2  41457  dihjatcclem4  41459  dihjat  41461  dihjat3  41470  dihjat5N  41475  dvh4dimat  41476