Theorem atbase 39253

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3459  ∅c0 4308   class class class wbr 5119  ‘cfv 6530  Basecbs 17226  0.cp0 18431   ⋖ ccvr 39226  Atomscatm 39227

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6483  df-fun 6532  df-fv 6538  df-ats 39231

This theorem is referenced by:  atssbase  39254  0ltat  39255  leatb  39256  meetat  39260  atnle0  39273  atlen0  39274  atcmp  39275  atcvreq0  39278  atncvrN  39279  atnle  39281  atnem0  39282  atlatmstc  39283  atlatle  39284  cvlexch2  39293  cvlexchb1  39294  cvlexchb2  39295  cvlatexchb1  39298  cvlatexchb2  39299  cvlatexch1  39300  cvlatexch2  39301  cvlatexch3  39302  cvlcvr1  39303  cvlcvrp  39304  cvlatcvr1  39305  cvlatcvr2  39306  cvlsupr2  39307  cvlsupr7  39312  cvlsupr8  39313  hlatjcl  39331  hlatjcom  39332  hlatjidm  39333  hlatjass  39334  hlatj32  39336  hlatj4  39338  hlatlej1  39339  atnlej1  39344  atnlej2  39345  hlrelat5N  39366  hlrelat  39367  hlrelat2  39368  exatleN  39369  cvr2N  39376  hlrelat3  39377  cvrval3  39378  cvrval5  39380  cvrexchlem  39384  cvratlem  39386  cvrat  39387  atcvr0eq  39391  lnnat  39392  cvrat2  39394  atcvrneN  39395  atcvrj1  39396  atcvrj2b  39397  atltcvr  39400  atle  39401  atlelt  39403  2atlt  39404  atexchcvrN  39405  cvrat3  39407  cvrat4  39408  cvrat42  39409  2atjm  39410  atbtwn  39411  3noncolr2  39414  4noncolr3  39418  athgt  39421  3dim0  39422  3dimlem3a  39425  3dimlem3OLDN  39427  3dimlem4a  39428  3dimlem4OLDN  39430  3dim3  39434  2dim  39435  1cvratex  39438  1cvrjat  39440  1cvrat  39441  ps-1  39442  ps-2  39443  hlatexch3N  39445  hlatexch4  39446  ps-2b  39447  3atlem1  39448  3atlem2  39449  3atlem4  39451  3atlem5  39452  3atlem6  39453  3at  39455  islln3  39475  llnnleat  39478  llnn0  39481  llnle  39483  llnexatN  39486  llncmp  39487  2llnmat  39489  2at0mat0  39490  2atm  39492  ps-2c  39493  lplni2  39502  lplnle  39505  lplnnle2at  39506  lplnn0N  39512  islpln2a  39513  2atmat  39526  lplnexllnN  39529  2llnjaN  39531  2llnm4  39535  2llnmeqat  39536  lvoli3  39542  islvol5  39544  lvoli2  39546  lvolnle3at  39547  3atnelvolN  39551  lvoln0N  39556  islvol2aN  39557  4atlem3  39561  4atlem3a  39562  4atlem3b  39563  4atlem4a  39564  4atlem4b  39565  4atlem4c  39566  4atlem4d  39567  4atlem9  39568  4atlem10a  39569  4atlem10  39571  4atlem11a  39572  4atlem11b  39573  4atlem11  39574  4atlem12a  39575  4atlem12b  39576  4atlem12  39577  4at2  39579  lplncvrlvol2  39580  2lplnja  39584  dalempeb  39604  dalemqeb  39605  dalemreb  39606  dalemseb  39607  dalemteb  39608  dalemueb  39609  dalem3  39629  dalem16  39644  dalemcceb  39654  dalem21  39659  dalem25  39663  dalem38  39675  dalem39  39676  dalem43  39680  dalem44  39681  dalem45  39682  dalem53  39690  dalem54  39691  dalem55  39692  dalem57  39694  dalem60  39697  snatpsubN  39715  linepsubN  39717  pmaple  39726  pmapat  39728  pmap1N  39732  pmapsub  39733  pmapglbx  39734  isline2  39739  linepmap  39740  isline3  39741  isline4N  39742  lneq2at  39743  lncvrelatN  39746  lncmp  39748  2lnat  39749  2atm2atN  39750  2llnma1b  39751  2llnma1  39752  2llnma3r  39753  cdlema1N  39756  cdlemblem  39758  cdlemb  39759  elpaddn0  39765  paddcom  39778  paddasslem2  39786  paddasslem5  39789  paddasslem12  39796  paddasslem13  39797  pmapjoin  39817  pmapjat1  39818  pmapjat2  39819  pmapjlln1  39820  atmod1i1  39822  atmod1i2  39824  llnmod1i2  39825  atmod2i1  39826  atmod2i2  39827  atmod3i1  39829  atmod3i2  39830  atmod4i1  39831  atmod4i2  39832  llnexchb2lem  39833  llnexchb2  39834  dalawlem2  39837  dalawlem3  39838  dalawlem5  39840  dalawlem6  39841  dalawlem7  39842  dalawlem8  39843  dalawlem11  39846  dalawlem12  39847  polval2N  39871  pol1N  39875  polatN  39896  2polatN  39897  paddatclN  39914  linepsubclN  39916  lhp2lt  39966  lhp0lt  39968  lhpexle2lem  39974  lhpexle3lem  39976  lhpjat2  39986  lhpj1  39987  lhpmcvr3  39990  lhpmcvr4N  39991  lhpmcvr5N  39992  lhpmcvr6N  39993  lhpmatb  39996  lhp2at0  39997  lhp2atnle  39998  lhp2at0nle  40000  lhprelat3N  40005  lhple  40007  lhpat4N  40009  lhpat3  40011  4atexlemtlw  40032  4atexlemc  40034  4atexlemnclw  40035  4atexlemcnd  40037  4atex2-0aOLDN  40043  lauteq  40060  ltrnid  40100  ltrnel  40104  ltrnat  40105  ltrncnvat  40106  ltrncnvel  40107  ltrncoval  40110  ltrncnv  40111  ltrn11at  40112  ltrneq2  40113  ltrneq  40114  idltrn  40115  trlval2  40128  trlcnv  40130  trljat1  40131  trljat2  40132  ltrnideq  40140  arglem1N  40155  cdlemc1  40156  cdlemc2  40157  cdlemc4  40159  cdlemc5  40160  cdlemc6  40161  cdlemd1  40163  cdlemd2  40164  cdlemd3  40165  cdlemd4  40166  cdlemd7  40169  cdleme0aa  40175  cdleme0b  40177  cdleme0c  40178  cdleme0cp  40179  cdleme0cq  40180  cdleme0e  40182  cdleme0fN  40183  cdleme1b  40191  cdleme1  40192  cdleme2  40193  cdleme3b  40194  cdleme3c  40195  cdleme3e  40197  cdleme3g  40199  cdleme3h  40200  cdleme3  40202  cdleme5  40205  cdleme7d  40211  cdleme7e  40212  cdleme7ga  40213  cdleme7  40214  cdleme8  40215  cdleme9  40218  cdleme10  40219  cdleme11c  40226  cdleme11e  40228  cdleme11fN  40229  cdleme11g  40230  cdleme11k  40233  cdleme11  40235  cdleme15b  40240  cdleme15  40243  cdleme16b  40244  cdleme17b  40252  cdleme17c  40253  cdlemednpq  40264  cdleme20zN  40266  cdleme19a  40268  cdleme20bN  40275  cdleme20d  40277  cdleme20j  40283  cdleme21c  40292  cdleme22aa  40304  cdleme22b  40306  cdleme22cN  40307  cdleme22d  40308  cdleme22e  40309  cdleme22eALTN  40310  cdleme23b  40315  cdleme23c  40316  cdleme27N  40334  cdleme28a  40335  cdleme30a  40343  cdlemefrs29pre00  40360  cdlemefrs29bpre0  40361  cdlemefrs29cpre1  40363  cdlemefrs32fva  40365  cdlemefrs32fva1  40366  cdlemefr32snb  40370  cdlemefs32snb  40380  cdleme32snb  40401  cdleme32fva  40402  cdleme32fva1  40403  cdleme32fvaw  40404  cdleme35a  40413  cdleme35fnpq  40414  cdleme35b  40415  cdleme35c  40416  cdleme35f  40419  cdleme42c  40437  cdleme42e  40444  cdleme42h  40447  cdleme42i  40448  cdleme42ke  40450  cdleme42keg  40451  cdleme42mgN  40453  cdleme17d4  40462  cdleme48fvg  40465  cdleme48bw  40467  cdlemeg46req  40494  cdleme50trn3  40518  cdlemf1  40526  cdlemf2  40527  trlord  40534  ltrniotacnvval  40547  cdlemg2fv2  40565  cdlemg2l  40568  cdlemg7fvbwN  40572  cdlemg4c  40577  cdlemg4  40582  cdlemg6c  40585  cdlemg8b  40593  cdlemg11b  40607  cdlemg13a  40616  cdlemg17a  40626  cdlemg17h  40633  cdlemg17  40642  cdlemg18b  40644  cdlemg19a  40648  cdlemg27a  40657  cdlemg27b  40661  cdlemg31a  40662  cdlemg31b  40663  cdlemg31d  40665  cdlemg33b0  40666  cdlemg33a  40671  cdlemg35  40678  trlcolem  40691  cdlemg42  40694  cdlemg44a  40696  cdlemg46  40700  cdlemh1  40780  cdlemh2  40781  cdlemh  40782  cdlemi1  40783  cdlemi  40785  cdlemk3  40798  cdlemk4  40799  cdlemkvcl  40807  cdlemk7  40813  cdlemk11  40814  cdlemk15  40820  cdlemk1u  40824  cdlemk7u  40835  cdlemk11u  40836  cdlemk37  40879  cdlemk39  40881  cdlemkid1  40887  cdlemkid2  40889  cdlemk48  40915  cdlemk50  40917  cdlemk51  40918  cdlemk52  40919  dia2dimlem1  41029  dia2dimlem2  41030  dia2dimlem3  41031  dia2dimlem5  41033  dia2dimlem7  41035  dia2dimlem9  41037  dia2dimlem10  41038  dia2dimlem12  41040  dia2dimlem13  41041  cdlemm10N  41083  cdlemn2  41160  cdlemn3  41162  cdlemn9  41170  cdlemn10  41171  dihjustlem  41181  dihord1  41183  dihord2pre2  41191  dihvalcqat  41204  dib2dim  41208  dih2dimb  41209  dih2dimbALTN  41210  dihord5apre  41227  dihglbcpreN  41265  dihmeetlem3N  41270  dihmeetlem6  41274  dihjatc1  41276  dihjatc2N  41277  dihjatc3  41278  dihmeetlem9N  41280  dihmeetlem10N  41281  dihmeetlem11N  41282  dihmeetlem13N  41284  dihmeetlem15N  41286  dihmeetlem16N  41287  dihmeetlem17N  41288  dihatexv2  41304  dihjatb  41381  dihjatc  41382  dihjatcclem1  41383  dihjatcclem2  41384  dihjatcclem4  41386  dihjat  41388  dihjat3  41397  dihjat5N  41402  dvh4dimat  41403