Theorem atbase 39925

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 32605 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 4295	. . . 4 ⊢ (𝑃 ∈ 𝐴 → ¬ 𝐴 = ∅)
2		atombase.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
3	2	eqeq1i 2770	. . . 4 ⊢ (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
4	1, 3	sylnib 331	. . 3 ⊢ (𝑃 ∈ 𝐴 → ¬ (Atoms‘𝐾) = ∅)
5		fvprc 6863	. . 3 ⊢ (¬ 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
6	4, 5	nsyl2 142	. 2 ⊢ (𝑃 ∈ 𝐴 → 𝐾 ∈ V)
7		atombase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2765	. . . 4 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		eqid 2765	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	isat 39922	. . 3 ⊢ (𝐾 ∈ V → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
11	10	simprbda 503	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐵)
12	6, 11	mpancom 700	1 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  Vcvv 3457  ∅c0 4288   class class class wbr 5105  ‘cfv 6525  Basecbs 17259  0.cp0 18467   ⋖ ccvr 39898  Atomscatm 39899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-iota 6481  df-fun 6527  df-fv 6533  df-ats 39903

This theorem is referenced by:  atssbase  39926  0ltat  39927  leatb  39928  meetat  39932  atnle0  39945  atlen0  39946  atcmp  39947  atcvreq0  39950  atncvrN  39951  atnle  39953  atnem0  39954  atlatmstc  39955  atlatle  39956  cvlexch2  39965  cvlexchb1  39966  cvlexchb2  39967  cvlatexchb1  39970  cvlatexchb2  39971  cvlatexch1  39972  cvlatexch2  39973  cvlatexch3  39974  cvlcvr1  39975  cvlcvrp  39976  cvlatcvr1  39977  cvlatcvr2  39978  cvlsupr2  39979  cvlsupr7  39984  cvlsupr8  39985  hlatjcl  40003  hlatjcom  40004  hlatjidm  40005  hlatjass  40006  hlatj32  40008  hlatj4  40010  hlatlej1  40011  atnlej1  40015  atnlej2  40016  hlrelat5N  40037  hlrelat  40038  hlrelat2  40039  exatleN  40040  cvr2N  40047  hlrelat3  40048  cvrval3  40049  cvrval5  40051  cvrexchlem  40055  cvratlem  40057  cvrat  40058  atcvr0eq  40062  lnnat  40063  cvrat2  40065  atcvrneN  40066  atcvrj1  40067  atcvrj2b  40068  atltcvr  40071  atle  40072  atlelt  40074  2atlt  40075  atexchcvrN  40076  cvrat3  40078  cvrat4  40079  cvrat42  40080  2atjm  40081  atbtwn  40082  3noncolr2  40085  4noncolr3  40089  athgt  40092  3dim0  40093  3dimlem3a  40096  3dimlem3OLDN  40098  3dimlem4a  40099  3dimlem4OLDN  40101  3dim3  40105  2dim  40106  1cvratex  40109  1cvrjat  40111  1cvrat  40112  ps-1  40113  ps-2  40114  hlatexch3N  40116  hlatexch4  40117  ps-2b  40118  3atlem1  40119  3atlem2  40120  3atlem4  40122  3atlem5  40123  3atlem6  40124  3at  40126  islln3  40146  llnnleat  40149  llnn0  40152  llnle  40154  llnexatN  40157  llncmp  40158  2llnmat  40160  2at0mat0  40161  2atm  40163  ps-2c  40164  lplni2  40173  lplnle  40176  lplnnle2at  40177  lplnn0N  40183  islpln2a  40184  2atmat  40197  lplnexllnN  40200  2llnjaN  40202  2llnm4  40206  2llnmeqat  40207  lvoli3  40213  islvol5  40215  lvoli2  40217  lvolnle3at  40218  3atnelvolN  40222  lvoln0N  40227  islvol2aN  40228  4atlem3  40232  4atlem3a  40233  4atlem3b  40234  4atlem4a  40235  4atlem4b  40236  4atlem4c  40237  4atlem4d  40238  4atlem9  40239  4atlem10a  40240  4atlem10  40242  4atlem11a  40243  4atlem11b  40244  4atlem11  40245  4atlem12a  40246  4atlem12b  40247  4atlem12  40248  4at2  40250  lplncvrlvol2  40251  2lplnja  40255  dalempeb  40275  dalemqeb  40276  dalemreb  40277  dalemseb  40278  dalemteb  40279  dalemueb  40280  dalem3  40300  dalem16  40315  dalemcceb  40325  dalem21  40330  dalem25  40334  dalem38  40346  dalem39  40347  dalem43  40351  dalem44  40352  dalem45  40353  dalem53  40361  dalem54  40362  dalem55  40363  dalem57  40365  dalem60  40368  snatpsubN  40386  linepsubN  40388  pmaple  40397  pmapat  40399  pmap1N  40403  pmapsub  40404  pmapglbx  40405  isline2  40410  linepmap  40411  isline3  40412  isline4N  40413  lneq2at  40414  lncvrelatN  40417  lncmp  40419  2lnat  40420  2atm2atN  40421  2llnma1b  40422  2llnma1  40423  2llnma3r  40424  cdlema1N  40427  cdlemblem  40429  cdlemb  40430  elpaddn0  40436  paddcom  40449  paddasslem2  40457  paddasslem5  40460  paddasslem12  40467  paddasslem13  40468  pmapjoin  40488  pmapjat1  40489  pmapjat2  40490  pmapjlln1  40491  atmod1i1  40493  atmod1i2  40495  llnmod1i2  40496  atmod2i1  40497  atmod2i2  40498  atmod3i1  40500  atmod3i2  40501  atmod4i1  40502  atmod4i2  40503  llnexchb2lem  40504  llnexchb2  40505  dalawlem2  40508  dalawlem3  40509  dalawlem5  40511  dalawlem6  40512  dalawlem7  40513  dalawlem8  40514  dalawlem11  40517  dalawlem12  40518  polval2N  40542  pol1N  40546  polatN  40567  2polatN  40568  paddatclN  40585  linepsubclN  40587  lhp2lt  40637  lhp0lt  40639  lhpexle2lem  40645  lhpexle3lem  40647  lhpjat2  40657  lhpj1  40658  lhpmcvr3  40661  lhpmcvr4N  40662  lhpmcvr5N  40663  lhpmcvr6N  40664  lhpmatb  40667  lhp2at0  40668  lhp2atnle  40669  lhp2at0nle  40671  lhprelat3N  40676  lhple  40678  lhpat4N  40680  lhpat3  40682  4atexlemtlw  40703  4atexlemc  40705  4atexlemnclw  40706  4atexlemcnd  40708  4atex2-0aOLDN  40714  lauteq  40731  ltrnid  40771  ltrnel  40775  ltrnat  40776  ltrncnvat  40777  ltrncnvel  40778  ltrncoval  40781  ltrncnv  40782  ltrn11at  40783  ltrneq2  40784  ltrneq  40785  idltrn  40786  trlval2  40799  trlcnv  40801  trljat1  40802  trljat2  40803  ltrnideq  40811  arglem1N  40826  cdlemc1  40827  cdlemc2  40828  cdlemc4  40830  cdlemc5  40831  cdlemc6  40832  cdlemd1  40834  cdlemd2  40835  cdlemd3  40836  cdlemd4  40837  cdlemd7  40840  cdleme0aa  40846  cdleme0b  40848  cdleme0c  40849  cdleme0cp  40850  cdleme0cq  40851  cdleme0e  40853  cdleme0fN  40854  cdleme1b  40862  cdleme1  40863  cdleme2  40864  cdleme3b  40865  cdleme3c  40866  cdleme3e  40868  cdleme3g  40870  cdleme3h  40871  cdleme3  40873  cdleme5  40876  cdleme7d  40882  cdleme7e  40883  cdleme7ga  40884  cdleme7  40885  cdleme8  40886  cdleme9  40889  cdleme10  40890  cdleme11c  40897  cdleme11e  40899  cdleme11fN  40900  cdleme11g  40901  cdleme11k  40904  cdleme11  40906  cdleme15b  40911  cdleme15  40914  cdleme16b  40915  cdleme17b  40923  cdleme17c  40924  cdlemednpq  40935  cdleme20zN  40937  cdleme19a  40939  cdleme20bN  40946  cdleme20d  40948  cdleme20j  40954  cdleme21c  40963  cdleme22aa  40975  cdleme22b  40977  cdleme22cN  40978  cdleme22d  40979  cdleme22e  40980  cdleme22eALTN  40981  cdleme23b  40986  cdleme23c  40987  cdleme27N  41005  cdleme28a  41006  cdleme30a  41014  cdlemefrs29pre00  41031  cdlemefrs29bpre0  41032  cdlemefrs29cpre1  41034  cdlemefrs32fva  41036  cdlemefrs32fva1  41037  cdlemefr32snb  41041  cdlemefs32snb  41051  cdleme32snb  41072  cdleme32fva  41073  cdleme32fva1  41074  cdleme32fvaw  41075  cdleme35a  41084  cdleme35fnpq  41085  cdleme35b  41086  cdleme35c  41087  cdleme35f  41090  cdleme42c  41108  cdleme42e  41115  cdleme42h  41118  cdleme42i  41119  cdleme42ke  41121  cdleme42keg  41122  cdleme42mgN  41124  cdleme17d4  41133  cdleme48fvg  41136  cdleme48bw  41138  cdlemeg46req  41165  cdleme50trn3  41189  cdlemf1  41197  cdlemf2  41198  trlord  41205  ltrniotacnvval  41218  cdlemg2fv2  41236  cdlemg2l  41239  cdlemg7fvbwN  41243  cdlemg4c  41248  cdlemg4  41253  cdlemg6c  41256  cdlemg8b  41264  cdlemg11b  41278  cdlemg13a  41287  cdlemg17a  41297  cdlemg17h  41304  cdlemg17  41313  cdlemg18b  41315  cdlemg19a  41319  cdlemg27a  41328  cdlemg27b  41332  cdlemg31a  41333  cdlemg31b  41334  cdlemg31d  41336  cdlemg33b0  41337  cdlemg33a  41342  cdlemg35  41349  trlcolem  41362  cdlemg42  41365  cdlemg44a  41367  cdlemg46  41371  cdlemh1  41451  cdlemh2  41452  cdlemh  41453  cdlemi1  41454  cdlemi  41456  cdlemk3  41469  cdlemk4  41470  cdlemkvcl  41478  cdlemk7  41484  cdlemk11  41485  cdlemk15  41491  cdlemk1u  41495  cdlemk7u  41506  cdlemk11u  41507  cdlemk37  41550  cdlemk39  41552  cdlemkid1  41558  cdlemkid2  41560  cdlemk48  41586  cdlemk50  41588  cdlemk51  41589  cdlemk52  41590  dia2dimlem1  41700  dia2dimlem2  41701  dia2dimlem3  41702  dia2dimlem5  41704  dia2dimlem7  41706  dia2dimlem9  41708  dia2dimlem10  41709  dia2dimlem12  41711  dia2dimlem13  41712  cdlemm10N  41754  cdlemn2  41831  cdlemn3  41833  cdlemn9  41841  cdlemn10  41842  dihjustlem  41852  dihord1  41854  dihord2pre2  41862  dihvalcqat  41875  dib2dim  41879  dih2dimb  41880  dih2dimbALTN  41881  dihord5apre  41898  dihglbcpreN  41936  dihmeetlem3N  41941  dihmeetlem6  41945  dihjatc1  41947  dihjatc2N  41948  dihjatc3  41949  dihmeetlem9N  41951  dihmeetlem10N  41952  dihmeetlem11N  41953  dihmeetlem13N  41955  dihmeetlem15N  41957  dihmeetlem16N  41958  dihmeetlem17N  41959  dihatexv2  41975  dihjatb  42052  dihjatc  42053  dihjatcclem1  42054  dihjatcclem2  42055  dihjatcclem4  42057  dihjat  42059  dihjat3  42068  dihjat5N  42073  dvh4dimat  42074