Theorem atbase 39289

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 32280 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 4306	. . . 4 ⊢ (𝑃 ∈ 𝐴 → ¬ 𝐴 = ∅)
2		atombase.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
3	2	eqeq1i 2735	. . . 4 ⊢ (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
4	1, 3	sylnib 328	. . 3 ⊢ (𝑃 ∈ 𝐴 → ¬ (Atoms‘𝐾) = ∅)
5		fvprc 6853	. . 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 39286	. . 3 ⊢ (𝐾 ∈ V → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
11	10	simprbda 498	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐵)
12	6, 11	mpancom 688	1 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3450  ∅c0 4299   class class class wbr 5110  ‘cfv 6514  Basecbs 17186  0.cp0 18389   ⋖ ccvr 39262  Atomscatm 39263

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522  df-ats 39267

This theorem is referenced by:  atssbase  39290  0ltat  39291  leatb  39292  meetat  39296  atnle0  39309  atlen0  39310  atcmp  39311  atcvreq0  39314  atncvrN  39315  atnle  39317  atnem0  39318  atlatmstc  39319  atlatle  39320  cvlexch2  39329  cvlexchb1  39330  cvlexchb2  39331  cvlatexchb1  39334  cvlatexchb2  39335  cvlatexch1  39336  cvlatexch2  39337  cvlatexch3  39338  cvlcvr1  39339  cvlcvrp  39340  cvlatcvr1  39341  cvlatcvr2  39342  cvlsupr2  39343  cvlsupr7  39348  cvlsupr8  39349  hlatjcl  39367  hlatjcom  39368  hlatjidm  39369  hlatjass  39370  hlatj32  39372  hlatj4  39374  hlatlej1  39375  atnlej1  39380  atnlej2  39381  hlrelat5N  39402  hlrelat  39403  hlrelat2  39404  exatleN  39405  cvr2N  39412  hlrelat3  39413  cvrval3  39414  cvrval5  39416  cvrexchlem  39420  cvratlem  39422  cvrat  39423  atcvr0eq  39427  lnnat  39428  cvrat2  39430  atcvrneN  39431  atcvrj1  39432  atcvrj2b  39433  atltcvr  39436  atle  39437  atlelt  39439  2atlt  39440  atexchcvrN  39441  cvrat3  39443  cvrat4  39444  cvrat42  39445  2atjm  39446  atbtwn  39447  3noncolr2  39450  4noncolr3  39454  athgt  39457  3dim0  39458  3dimlem3a  39461  3dimlem3OLDN  39463  3dimlem4a  39464  3dimlem4OLDN  39466  3dim3  39470  2dim  39471  1cvratex  39474  1cvrjat  39476  1cvrat  39477  ps-1  39478  ps-2  39479  hlatexch3N  39481  hlatexch4  39482  ps-2b  39483  3atlem1  39484  3atlem2  39485  3atlem4  39487  3atlem5  39488  3atlem6  39489  3at  39491  islln3  39511  llnnleat  39514  llnn0  39517  llnle  39519  llnexatN  39522  llncmp  39523  2llnmat  39525  2at0mat0  39526  2atm  39528  ps-2c  39529  lplni2  39538  lplnle  39541  lplnnle2at  39542  lplnn0N  39548  islpln2a  39549  2atmat  39562  lplnexllnN  39565  2llnjaN  39567  2llnm4  39571  2llnmeqat  39572  lvoli3  39578  islvol5  39580  lvoli2  39582  lvolnle3at  39583  3atnelvolN  39587  lvoln0N  39592  islvol2aN  39593  4atlem3  39597  4atlem3a  39598  4atlem3b  39599  4atlem4a  39600  4atlem4b  39601  4atlem4c  39602  4atlem4d  39603  4atlem9  39604  4atlem10a  39605  4atlem10  39607  4atlem11a  39608  4atlem11b  39609  4atlem11  39610  4atlem12a  39611  4atlem12b  39612  4atlem12  39613  4at2  39615  lplncvrlvol2  39616  2lplnja  39620  dalempeb  39640  dalemqeb  39641  dalemreb  39642  dalemseb  39643  dalemteb  39644  dalemueb  39645  dalem3  39665  dalem16  39680  dalemcceb  39690  dalem21  39695  dalem25  39699  dalem38  39711  dalem39  39712  dalem43  39716  dalem44  39717  dalem45  39718  dalem53  39726  dalem54  39727  dalem55  39728  dalem57  39730  dalem60  39733  snatpsubN  39751  linepsubN  39753  pmaple  39762  pmapat  39764  pmap1N  39768  pmapsub  39769  pmapglbx  39770  isline2  39775  linepmap  39776  isline3  39777  isline4N  39778  lneq2at  39779  lncvrelatN  39782  lncmp  39784  2lnat  39785  2atm2atN  39786  2llnma1b  39787  2llnma1  39788  2llnma3r  39789  cdlema1N  39792  cdlemblem  39794  cdlemb  39795  elpaddn0  39801  paddcom  39814  paddasslem2  39822  paddasslem5  39825  paddasslem12  39832  paddasslem13  39833  pmapjoin  39853  pmapjat1  39854  pmapjat2  39855  pmapjlln1  39856  atmod1i1  39858  atmod1i2  39860  llnmod1i2  39861  atmod2i1  39862  atmod2i2  39863  atmod3i1  39865  atmod3i2  39866  atmod4i1  39867  atmod4i2  39868  llnexchb2lem  39869  llnexchb2  39870  dalawlem2  39873  dalawlem3  39874  dalawlem5  39876  dalawlem6  39877  dalawlem7  39878  dalawlem8  39879  dalawlem11  39882  dalawlem12  39883  polval2N  39907  pol1N  39911  polatN  39932  2polatN  39933  paddatclN  39950  linepsubclN  39952  lhp2lt  40002  lhp0lt  40004  lhpexle2lem  40010  lhpexle3lem  40012  lhpjat2  40022  lhpj1  40023  lhpmcvr3  40026  lhpmcvr4N  40027  lhpmcvr5N  40028  lhpmcvr6N  40029  lhpmatb  40032  lhp2at0  40033  lhp2atnle  40034  lhp2at0nle  40036  lhprelat3N  40041  lhple  40043  lhpat4N  40045  lhpat3  40047  4atexlemtlw  40068  4atexlemc  40070  4atexlemnclw  40071  4atexlemcnd  40073  4atex2-0aOLDN  40079  lauteq  40096  ltrnid  40136  ltrnel  40140  ltrnat  40141  ltrncnvat  40142  ltrncnvel  40143  ltrncoval  40146  ltrncnv  40147  ltrn11at  40148  ltrneq2  40149  ltrneq  40150  idltrn  40151  trlval2  40164  trlcnv  40166  trljat1  40167  trljat2  40168  ltrnideq  40176  arglem1N  40191  cdlemc1  40192  cdlemc2  40193  cdlemc4  40195  cdlemc5  40196  cdlemc6  40197  cdlemd1  40199  cdlemd2  40200  cdlemd3  40201  cdlemd4  40202  cdlemd7  40205  cdleme0aa  40211  cdleme0b  40213  cdleme0c  40214  cdleme0cp  40215  cdleme0cq  40216  cdleme0e  40218  cdleme0fN  40219  cdleme1b  40227  cdleme1  40228  cdleme2  40229  cdleme3b  40230  cdleme3c  40231  cdleme3e  40233  cdleme3g  40235  cdleme3h  40236  cdleme3  40238  cdleme5  40241  cdleme7d  40247  cdleme7e  40248  cdleme7ga  40249  cdleme7  40250  cdleme8  40251  cdleme9  40254  cdleme10  40255  cdleme11c  40262  cdleme11e  40264  cdleme11fN  40265  cdleme11g  40266  cdleme11k  40269  cdleme11  40271  cdleme15b  40276  cdleme15  40279  cdleme16b  40280  cdleme17b  40288  cdleme17c  40289  cdlemednpq  40300  cdleme20zN  40302  cdleme19a  40304  cdleme20bN  40311  cdleme20d  40313  cdleme20j  40319  cdleme21c  40328  cdleme22aa  40340  cdleme22b  40342  cdleme22cN  40343  cdleme22d  40344  cdleme22e  40345  cdleme22eALTN  40346  cdleme23b  40351  cdleme23c  40352  cdleme27N  40370  cdleme28a  40371  cdleme30a  40379  cdlemefrs29pre00  40396  cdlemefrs29bpre0  40397  cdlemefrs29cpre1  40399  cdlemefrs32fva  40401  cdlemefrs32fva1  40402  cdlemefr32snb  40406  cdlemefs32snb  40416  cdleme32snb  40437  cdleme32fva  40438  cdleme32fva1  40439  cdleme32fvaw  40440  cdleme35a  40449  cdleme35fnpq  40450  cdleme35b  40451  cdleme35c  40452  cdleme35f  40455  cdleme42c  40473  cdleme42e  40480  cdleme42h  40483  cdleme42i  40484  cdleme42ke  40486  cdleme42keg  40487  cdleme42mgN  40489  cdleme17d4  40498  cdleme48fvg  40501  cdleme48bw  40503  cdlemeg46req  40530  cdleme50trn3  40554  cdlemf1  40562  cdlemf2  40563  trlord  40570  ltrniotacnvval  40583  cdlemg2fv2  40601  cdlemg2l  40604  cdlemg7fvbwN  40608  cdlemg4c  40613  cdlemg4  40618  cdlemg6c  40621  cdlemg8b  40629  cdlemg11b  40643  cdlemg13a  40652  cdlemg17a  40662  cdlemg17h  40669  cdlemg17  40678  cdlemg18b  40680  cdlemg19a  40684  cdlemg27a  40693  cdlemg27b  40697  cdlemg31a  40698  cdlemg31b  40699  cdlemg31d  40701  cdlemg33b0  40702  cdlemg33a  40707  cdlemg35  40714  trlcolem  40727  cdlemg42  40730  cdlemg44a  40732  cdlemg46  40736  cdlemh1  40816  cdlemh2  40817  cdlemh  40818  cdlemi1  40819  cdlemi  40821  cdlemk3  40834  cdlemk4  40835  cdlemkvcl  40843  cdlemk7  40849  cdlemk11  40850  cdlemk15  40856  cdlemk1u  40860  cdlemk7u  40871  cdlemk11u  40872  cdlemk37  40915  cdlemk39  40917  cdlemkid1  40923  cdlemkid2  40925  cdlemk48  40951  cdlemk50  40953  cdlemk51  40954  cdlemk52  40955  dia2dimlem1  41065  dia2dimlem2  41066  dia2dimlem3  41067  dia2dimlem5  41069  dia2dimlem7  41071  dia2dimlem9  41073  dia2dimlem10  41074  dia2dimlem12  41076  dia2dimlem13  41077  cdlemm10N  41119  cdlemn2  41196  cdlemn3  41198  cdlemn9  41206  cdlemn10  41207  dihjustlem  41217  dihord1  41219  dihord2pre2  41227  dihvalcqat  41240  dib2dim  41244  dih2dimb  41245  dih2dimbALTN  41246  dihord5apre  41263  dihglbcpreN  41301  dihmeetlem3N  41306  dihmeetlem6  41310  dihjatc1  41312  dihjatc2N  41313  dihjatc3  41314  dihmeetlem9N  41316  dihmeetlem10N  41317  dihmeetlem11N  41318  dihmeetlem13N  41320  dihmeetlem15N  41322  dihmeetlem16N  41323  dihmeetlem17N  41324  dihatexv2  41340  dihjatb  41417  dihjatc  41418  dihjatcclem1  41419  dihjatcclem2  41420  dihjatcclem4  41422  dihjat  41424  dihjat3  41433  dihjat5N  41438  dvh4dimat  41439