Theorem atbase 39408

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3437  ∅c0 4282   class class class wbr 5093  ‘cfv 6486  Basecbs 17122  0.cp0 18329   ⋖ ccvr 39381  Atomscatm 39382

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6442  df-fun 6488  df-fv 6494  df-ats 39386

This theorem is referenced by:  atssbase  39409  0ltat  39410  leatb  39411  meetat  39415  atnle0  39428  atlen0  39429  atcmp  39430  atcvreq0  39433  atncvrN  39434  atnle  39436  atnem0  39437  atlatmstc  39438  atlatle  39439  cvlexch2  39448  cvlexchb1  39449  cvlexchb2  39450  cvlatexchb1  39453  cvlatexchb2  39454  cvlatexch1  39455  cvlatexch2  39456  cvlatexch3  39457  cvlcvr1  39458  cvlcvrp  39459  cvlatcvr1  39460  cvlatcvr2  39461  cvlsupr2  39462  cvlsupr7  39467  cvlsupr8  39468  hlatjcl  39486  hlatjcom  39487  hlatjidm  39488  hlatjass  39489  hlatj32  39491  hlatj4  39493  hlatlej1  39494  atnlej1  39498  atnlej2  39499  hlrelat5N  39520  hlrelat  39521  hlrelat2  39522  exatleN  39523  cvr2N  39530  hlrelat3  39531  cvrval3  39532  cvrval5  39534  cvrexchlem  39538  cvratlem  39540  cvrat  39541  atcvr0eq  39545  lnnat  39546  cvrat2  39548  atcvrneN  39549  atcvrj1  39550  atcvrj2b  39551  atltcvr  39554  atle  39555  atlelt  39557  2atlt  39558  atexchcvrN  39559  cvrat3  39561  cvrat4  39562  cvrat42  39563  2atjm  39564  atbtwn  39565  3noncolr2  39568  4noncolr3  39572  athgt  39575  3dim0  39576  3dimlem3a  39579  3dimlem3OLDN  39581  3dimlem4a  39582  3dimlem4OLDN  39584  3dim3  39588  2dim  39589  1cvratex  39592  1cvrjat  39594  1cvrat  39595  ps-1  39596  ps-2  39597  hlatexch3N  39599  hlatexch4  39600  ps-2b  39601  3atlem1  39602  3atlem2  39603  3atlem4  39605  3atlem5  39606  3atlem6  39607  3at  39609  islln3  39629  llnnleat  39632  llnn0  39635  llnle  39637  llnexatN  39640  llncmp  39641  2llnmat  39643  2at0mat0  39644  2atm  39646  ps-2c  39647  lplni2  39656  lplnle  39659  lplnnle2at  39660  lplnn0N  39666  islpln2a  39667  2atmat  39680  lplnexllnN  39683  2llnjaN  39685  2llnm4  39689  2llnmeqat  39690  lvoli3  39696  islvol5  39698  lvoli2  39700  lvolnle3at  39701  3atnelvolN  39705  lvoln0N  39710  islvol2aN  39711  4atlem3  39715  4atlem3a  39716  4atlem3b  39717  4atlem4a  39718  4atlem4b  39719  4atlem4c  39720  4atlem4d  39721  4atlem9  39722  4atlem10a  39723  4atlem10  39725  4atlem11a  39726  4atlem11b  39727  4atlem11  39728  4atlem12a  39729  4atlem12b  39730  4atlem12  39731  4at2  39733  lplncvrlvol2  39734  2lplnja  39738  dalempeb  39758  dalemqeb  39759  dalemreb  39760  dalemseb  39761  dalemteb  39762  dalemueb  39763  dalem3  39783  dalem16  39798  dalemcceb  39808  dalem21  39813  dalem25  39817  dalem38  39829  dalem39  39830  dalem43  39834  dalem44  39835  dalem45  39836  dalem53  39844  dalem54  39845  dalem55  39846  dalem57  39848  dalem60  39851  snatpsubN  39869  linepsubN  39871  pmaple  39880  pmapat  39882  pmap1N  39886  pmapsub  39887  pmapglbx  39888  isline2  39893  linepmap  39894  isline3  39895  isline4N  39896  lneq2at  39897  lncvrelatN  39900  lncmp  39902  2lnat  39903  2atm2atN  39904  2llnma1b  39905  2llnma1  39906  2llnma3r  39907  cdlema1N  39910  cdlemblem  39912  cdlemb  39913  elpaddn0  39919  paddcom  39932  paddasslem2  39940  paddasslem5  39943  paddasslem12  39950  paddasslem13  39951  pmapjoin  39971  pmapjat1  39972  pmapjat2  39973  pmapjlln1  39974  atmod1i1  39976  atmod1i2  39978  llnmod1i2  39979  atmod2i1  39980  atmod2i2  39981  atmod3i1  39983  atmod3i2  39984  atmod4i1  39985  atmod4i2  39986  llnexchb2lem  39987  llnexchb2  39988  dalawlem2  39991  dalawlem3  39992  dalawlem5  39994  dalawlem6  39995  dalawlem7  39996  dalawlem8  39997  dalawlem11  40000  dalawlem12  40001  polval2N  40025  pol1N  40029  polatN  40050  2polatN  40051  paddatclN  40068  linepsubclN  40070  lhp2lt  40120  lhp0lt  40122  lhpexle2lem  40128  lhpexle3lem  40130  lhpjat2  40140  lhpj1  40141  lhpmcvr3  40144  lhpmcvr4N  40145  lhpmcvr5N  40146  lhpmcvr6N  40147  lhpmatb  40150  lhp2at0  40151  lhp2atnle  40152  lhp2at0nle  40154  lhprelat3N  40159  lhple  40161  lhpat4N  40163  lhpat3  40165  4atexlemtlw  40186  4atexlemc  40188  4atexlemnclw  40189  4atexlemcnd  40191  4atex2-0aOLDN  40197  lauteq  40214  ltrnid  40254  ltrnel  40258  ltrnat  40259  ltrncnvat  40260  ltrncnvel  40261  ltrncoval  40264  ltrncnv  40265  ltrn11at  40266  ltrneq2  40267  ltrneq  40268  idltrn  40269  trlval2  40282  trlcnv  40284  trljat1  40285  trljat2  40286  ltrnideq  40294  arglem1N  40309  cdlemc1  40310  cdlemc2  40311  cdlemc4  40313  cdlemc5  40314  cdlemc6  40315  cdlemd1  40317  cdlemd2  40318  cdlemd3  40319  cdlemd4  40320  cdlemd7  40323  cdleme0aa  40329  cdleme0b  40331  cdleme0c  40332  cdleme0cp  40333  cdleme0cq  40334  cdleme0e  40336  cdleme0fN  40337  cdleme1b  40345  cdleme1  40346  cdleme2  40347  cdleme3b  40348  cdleme3c  40349  cdleme3e  40351  cdleme3g  40353  cdleme3h  40354  cdleme3  40356  cdleme5  40359  cdleme7d  40365  cdleme7e  40366  cdleme7ga  40367  cdleme7  40368  cdleme8  40369  cdleme9  40372  cdleme10  40373  cdleme11c  40380  cdleme11e  40382  cdleme11fN  40383  cdleme11g  40384  cdleme11k  40387  cdleme11  40389  cdleme15b  40394  cdleme15  40397  cdleme16b  40398  cdleme17b  40406  cdleme17c  40407  cdlemednpq  40418  cdleme20zN  40420  cdleme19a  40422  cdleme20bN  40429  cdleme20d  40431  cdleme20j  40437  cdleme21c  40446  cdleme22aa  40458  cdleme22b  40460  cdleme22cN  40461  cdleme22d  40462  cdleme22e  40463  cdleme22eALTN  40464  cdleme23b  40469  cdleme23c  40470  cdleme27N  40488  cdleme28a  40489  cdleme30a  40497  cdlemefrs29pre00  40514  cdlemefrs29bpre0  40515  cdlemefrs29cpre1  40517  cdlemefrs32fva  40519  cdlemefrs32fva1  40520  cdlemefr32snb  40524  cdlemefs32snb  40534  cdleme32snb  40555  cdleme32fva  40556  cdleme32fva1  40557  cdleme32fvaw  40558  cdleme35a  40567  cdleme35fnpq  40568  cdleme35b  40569  cdleme35c  40570  cdleme35f  40573  cdleme42c  40591  cdleme42e  40598  cdleme42h  40601  cdleme42i  40602  cdleme42ke  40604  cdleme42keg  40605  cdleme42mgN  40607  cdleme17d4  40616  cdleme48fvg  40619  cdleme48bw  40621  cdlemeg46req  40648  cdleme50trn3  40672  cdlemf1  40680  cdlemf2  40681  trlord  40688  ltrniotacnvval  40701  cdlemg2fv2  40719  cdlemg2l  40722  cdlemg7fvbwN  40726  cdlemg4c  40731  cdlemg4  40736  cdlemg6c  40739  cdlemg8b  40747  cdlemg11b  40761  cdlemg13a  40770  cdlemg17a  40780  cdlemg17h  40787  cdlemg17  40796  cdlemg18b  40798  cdlemg19a  40802  cdlemg27a  40811  cdlemg27b  40815  cdlemg31a  40816  cdlemg31b  40817  cdlemg31d  40819  cdlemg33b0  40820  cdlemg33a  40825  cdlemg35  40832  trlcolem  40845  cdlemg42  40848  cdlemg44a  40850  cdlemg46  40854  cdlemh1  40934  cdlemh2  40935  cdlemh  40936  cdlemi1  40937  cdlemi  40939  cdlemk3  40952  cdlemk4  40953  cdlemkvcl  40961  cdlemk7  40967  cdlemk11  40968  cdlemk15  40974  cdlemk1u  40978  cdlemk7u  40989  cdlemk11u  40990  cdlemk37  41033  cdlemk39  41035  cdlemkid1  41041  cdlemkid2  41043  cdlemk48  41069  cdlemk50  41071  cdlemk51  41072  cdlemk52  41073  dia2dimlem1  41183  dia2dimlem2  41184  dia2dimlem3  41185  dia2dimlem5  41187  dia2dimlem7  41189  dia2dimlem9  41191  dia2dimlem10  41192  dia2dimlem12  41194  dia2dimlem13  41195  cdlemm10N  41237  cdlemn2  41314  cdlemn3  41316  cdlemn9  41324  cdlemn10  41325  dihjustlem  41335  dihord1  41337  dihord2pre2  41345  dihvalcqat  41358  dib2dim  41362  dih2dimb  41363  dih2dimbALTN  41364  dihord5apre  41381  dihglbcpreN  41419  dihmeetlem3N  41424  dihmeetlem6  41428  dihjatc1  41430  dihjatc2N  41431  dihjatc3  41432  dihmeetlem9N  41434  dihmeetlem10N  41435  dihmeetlem11N  41436  dihmeetlem13N  41438  dihmeetlem15N  41440  dihmeetlem16N  41441  dihmeetlem17N  41442  dihatexv2  41458  dihjatb  41535  dihjatc  41536  dihjatcclem1  41537  dihjatcclem2  41538  dihjatcclem4  41540  dihjat  41542  dihjat3  41551  dihjat5N  41556  dvh4dimat  41557