Theorem atbase 37299

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2110  Vcvv 3431  ∅c0 4262   class class class wbr 5079  ‘cfv 6432  Basecbs 16910  0.cp0 18139   ⋖ ccvr 37272  Atomscatm 37273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-iota 6390  df-fun 6434  df-fv 6440  df-ats 37277

This theorem is referenced by:  atssbase  37300  0ltat  37301  leatb  37302  meetat  37306  atnle0  37319  atlen0  37320  atcmp  37321  atcvreq0  37324  atncvrN  37325  atnle  37327  atnem0  37328  atlatmstc  37329  atlatle  37330  cvlexch2  37339  cvlexchb1  37340  cvlexchb2  37341  cvlatexchb1  37344  cvlatexchb2  37345  cvlatexch1  37346  cvlatexch2  37347  cvlatexch3  37348  cvlcvr1  37349  cvlcvrp  37350  cvlatcvr1  37351  cvlatcvr2  37352  cvlsupr2  37353  cvlsupr7  37358  cvlsupr8  37359  hlatjcl  37377  hlatjcom  37378  hlatjidm  37379  hlatjass  37380  hlatj32  37382  hlatj4  37384  hlatlej1  37385  atnlej1  37389  atnlej2  37390  hlrelat5N  37411  hlrelat  37412  hlrelat2  37413  exatleN  37414  cvr2N  37421  hlrelat3  37422  cvrval3  37423  cvrval5  37425  cvrexchlem  37429  cvratlem  37431  cvrat  37432  atcvr0eq  37436  lnnat  37437  cvrat2  37439  atcvrneN  37440  atcvrj1  37441  atcvrj2b  37442  atltcvr  37445  atle  37446  atlelt  37448  2atlt  37449  atexchcvrN  37450  cvrat3  37452  cvrat4  37453  cvrat42  37454  2atjm  37455  atbtwn  37456  3noncolr2  37459  4noncolr3  37463  athgt  37466  3dim0  37467  3dimlem3a  37470  3dimlem3OLDN  37472  3dimlem4a  37473  3dimlem4OLDN  37475  3dim3  37479  2dim  37480  1cvratex  37483  1cvrjat  37485  1cvrat  37486  ps-1  37487  ps-2  37488  hlatexch3N  37490  hlatexch4  37491  ps-2b  37492  3atlem1  37493  3atlem2  37494  3atlem4  37496  3atlem5  37497  3atlem6  37498  3at  37500  islln3  37520  llnnleat  37523  llnn0  37526  llnle  37528  llnexatN  37531  llncmp  37532  2llnmat  37534  2at0mat0  37535  2atm  37537  ps-2c  37538  lplni2  37547  lplnle  37550  lplnnle2at  37551  lplnn0N  37557  islpln2a  37558  2atmat  37571  lplnexllnN  37574  2llnjaN  37576  2llnm4  37580  2llnmeqat  37581  lvoli3  37587  islvol5  37589  lvoli2  37591  lvolnle3at  37592  3atnelvolN  37596  lvoln0N  37601  islvol2aN  37602  4atlem3  37606  4atlem3a  37607  4atlem3b  37608  4atlem4a  37609  4atlem4b  37610  4atlem4c  37611  4atlem4d  37612  4atlem9  37613  4atlem10a  37614  4atlem10  37616  4atlem11a  37617  4atlem11b  37618  4atlem11  37619  4atlem12a  37620  4atlem12b  37621  4atlem12  37622  4at2  37624  lplncvrlvol2  37625  2lplnja  37629  dalempeb  37649  dalemqeb  37650  dalemreb  37651  dalemseb  37652  dalemteb  37653  dalemueb  37654  dalem3  37674  dalem16  37689  dalemcceb  37699  dalem21  37704  dalem25  37708  dalem38  37720  dalem39  37721  dalem43  37725  dalem44  37726  dalem45  37727  dalem53  37735  dalem54  37736  dalem55  37737  dalem57  37739  dalem60  37742  snatpsubN  37760  linepsubN  37762  pmaple  37771  pmapat  37773  pmap1N  37777  pmapsub  37778  pmapglbx  37779  isline2  37784  linepmap  37785  isline3  37786  isline4N  37787  lneq2at  37788  lncvrelatN  37791  lncmp  37793  2lnat  37794  2atm2atN  37795  2llnma1b  37796  2llnma1  37797  2llnma3r  37798  cdlema1N  37801  cdlemblem  37803  cdlemb  37804  elpaddn0  37810  paddcom  37823  paddasslem2  37831  paddasslem5  37834  paddasslem12  37841  paddasslem13  37842  pmapjoin  37862  pmapjat1  37863  pmapjat2  37864  pmapjlln1  37865  atmod1i1  37867  atmod1i2  37869  llnmod1i2  37870  atmod2i1  37871  atmod2i2  37872  atmod3i1  37874  atmod3i2  37875  atmod4i1  37876  atmod4i2  37877  llnexchb2lem  37878  llnexchb2  37879  dalawlem2  37882  dalawlem3  37883  dalawlem5  37885  dalawlem6  37886  dalawlem7  37887  dalawlem8  37888  dalawlem11  37891  dalawlem12  37892  polval2N  37916  pol1N  37920  polatN  37941  2polatN  37942  paddatclN  37959  linepsubclN  37961  lhp2lt  38011  lhp0lt  38013  lhpexle2lem  38019  lhpexle3lem  38021  lhpjat2  38031  lhpj1  38032  lhpmcvr3  38035  lhpmcvr4N  38036  lhpmcvr5N  38037  lhpmcvr6N  38038  lhpmatb  38041  lhp2at0  38042  lhp2atnle  38043  lhp2at0nle  38045  lhprelat3N  38050  lhple  38052  lhpat4N  38054  lhpat3  38056  4atexlemtlw  38077  4atexlemc  38079  4atexlemnclw  38080  4atexlemcnd  38082  4atex2-0aOLDN  38088  lauteq  38105  ltrnid  38145  ltrnel  38149  ltrnat  38150  ltrncnvat  38151  ltrncnvel  38152  ltrncoval  38155  ltrncnv  38156  ltrn11at  38157  ltrneq2  38158  ltrneq  38159  idltrn  38160  trlval2  38173  trlcnv  38175  trljat1  38176  trljat2  38177  ltrnideq  38185  arglem1N  38200  cdlemc1  38201  cdlemc2  38202  cdlemc4  38204  cdlemc5  38205  cdlemc6  38206  cdlemd1  38208  cdlemd2  38209  cdlemd3  38210  cdlemd4  38211  cdlemd7  38214  cdleme0aa  38220  cdleme0b  38222  cdleme0c  38223  cdleme0cp  38224  cdleme0cq  38225  cdleme0e  38227  cdleme0fN  38228  cdleme1b  38236  cdleme1  38237  cdleme2  38238  cdleme3b  38239  cdleme3c  38240  cdleme3e  38242  cdleme3g  38244  cdleme3h  38245  cdleme3  38247  cdleme5  38250  cdleme7d  38256  cdleme7e  38257  cdleme7ga  38258  cdleme7  38259  cdleme8  38260  cdleme9  38263  cdleme10  38264  cdleme11c  38271  cdleme11e  38273  cdleme11fN  38274  cdleme11g  38275  cdleme11k  38278  cdleme11  38280  cdleme15b  38285  cdleme15  38288  cdleme16b  38289  cdleme17b  38297  cdleme17c  38298  cdlemednpq  38309  cdleme20zN  38311  cdleme19a  38313  cdleme20bN  38320  cdleme20d  38322  cdleme20j  38328  cdleme21c  38337  cdleme22aa  38349  cdleme22b  38351  cdleme22cN  38352  cdleme22d  38353  cdleme22e  38354  cdleme22eALTN  38355  cdleme23b  38360  cdleme23c  38361  cdleme27N  38379  cdleme28a  38380  cdleme30a  38388  cdlemefrs29pre00  38405  cdlemefrs29bpre0  38406  cdlemefrs29cpre1  38408  cdlemefrs32fva  38410  cdlemefrs32fva1  38411  cdlemefr32snb  38415  cdlemefs32snb  38425  cdleme32snb  38446  cdleme32fva  38447  cdleme32fva1  38448  cdleme32fvaw  38449  cdleme35a  38458  cdleme35fnpq  38459  cdleme35b  38460  cdleme35c  38461  cdleme35f  38464  cdleme42c  38482  cdleme42e  38489  cdleme42h  38492  cdleme42i  38493  cdleme42ke  38495  cdleme42keg  38496  cdleme42mgN  38498  cdleme17d4  38507  cdleme48fvg  38510  cdleme48bw  38512  cdlemeg46req  38539  cdleme50trn3  38563  cdlemf1  38571  cdlemf2  38572  trlord  38579  ltrniotacnvval  38592  cdlemg2fv2  38610  cdlemg2l  38613  cdlemg7fvbwN  38617  cdlemg4c  38622  cdlemg4  38627  cdlemg6c  38630  cdlemg8b  38638  cdlemg11b  38652  cdlemg13a  38661  cdlemg17a  38671  cdlemg17h  38678  cdlemg17  38687  cdlemg18b  38689  cdlemg19a  38693  cdlemg27a  38702  cdlemg27b  38706  cdlemg31a  38707  cdlemg31b  38708  cdlemg31d  38710  cdlemg33b0  38711  cdlemg33a  38716  cdlemg35  38723  trlcolem  38736  cdlemg42  38739  cdlemg44a  38741  cdlemg46  38745  cdlemh1  38825  cdlemh2  38826  cdlemh  38827  cdlemi1  38828  cdlemi  38830  cdlemk3  38843  cdlemk4  38844  cdlemkvcl  38852  cdlemk7  38858  cdlemk11  38859  cdlemk15  38865  cdlemk1u  38869  cdlemk7u  38880  cdlemk11u  38881  cdlemk37  38924  cdlemk39  38926  cdlemkid1  38932  cdlemkid2  38934  cdlemk48  38960  cdlemk50  38962  cdlemk51  38963  cdlemk52  38964  dia2dimlem1  39074  dia2dimlem2  39075  dia2dimlem3  39076  dia2dimlem5  39078  dia2dimlem7  39080  dia2dimlem9  39082  dia2dimlem10  39083  dia2dimlem12  39085  dia2dimlem13  39086  cdlemm10N  39128  cdlemn2  39205  cdlemn3  39207  cdlemn9  39215  cdlemn10  39216  dihjustlem  39226  dihord1  39228  dihord2pre2  39236  dihvalcqat  39249  dib2dim  39253  dih2dimb  39254  dih2dimbALTN  39255  dihord5apre  39272  dihglbcpreN  39310  dihmeetlem3N  39315  dihmeetlem6  39319  dihjatc1  39321  dihjatc2N  39322  dihjatc3  39323  dihmeetlem9N  39325  dihmeetlem10N  39326  dihmeetlem11N  39327  dihmeetlem13N  39329  dihmeetlem15N  39331  dihmeetlem16N  39332  dihmeetlem17N  39333  dihatexv2  39349  dihjatb  39426  dihjatc  39427  dihjatcclem1  39428  dihjatcclem2  39429  dihjatcclem4  39431  dihjat  39433  dihjat3  39442  dihjat5N  39447  dvh4dimat  39448