Theorem atbase 39290

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3480  ∅c0 4333   class class class wbr 5143  ‘cfv 6561  Basecbs 17247  0.cp0 18468   ⋖ ccvr 39263  Atomscatm 39264

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569  df-ats 39268

This theorem is referenced by:  atssbase  39291  0ltat  39292  leatb  39293  meetat  39297  atnle0  39310  atlen0  39311  atcmp  39312  atcvreq0  39315  atncvrN  39316  atnle  39318  atnem0  39319  atlatmstc  39320  atlatle  39321  cvlexch2  39330  cvlexchb1  39331  cvlexchb2  39332  cvlatexchb1  39335  cvlatexchb2  39336  cvlatexch1  39337  cvlatexch2  39338  cvlatexch3  39339  cvlcvr1  39340  cvlcvrp  39341  cvlatcvr1  39342  cvlatcvr2  39343  cvlsupr2  39344  cvlsupr7  39349  cvlsupr8  39350  hlatjcl  39368  hlatjcom  39369  hlatjidm  39370  hlatjass  39371  hlatj32  39373  hlatj4  39375  hlatlej1  39376  atnlej1  39381  atnlej2  39382  hlrelat5N  39403  hlrelat  39404  hlrelat2  39405  exatleN  39406  cvr2N  39413  hlrelat3  39414  cvrval3  39415  cvrval5  39417  cvrexchlem  39421  cvratlem  39423  cvrat  39424  atcvr0eq  39428  lnnat  39429  cvrat2  39431  atcvrneN  39432  atcvrj1  39433  atcvrj2b  39434  atltcvr  39437  atle  39438  atlelt  39440  2atlt  39441  atexchcvrN  39442  cvrat3  39444  cvrat4  39445  cvrat42  39446  2atjm  39447  atbtwn  39448  3noncolr2  39451  4noncolr3  39455  athgt  39458  3dim0  39459  3dimlem3a  39462  3dimlem3OLDN  39464  3dimlem4a  39465  3dimlem4OLDN  39467  3dim3  39471  2dim  39472  1cvratex  39475  1cvrjat  39477  1cvrat  39478  ps-1  39479  ps-2  39480  hlatexch3N  39482  hlatexch4  39483  ps-2b  39484  3atlem1  39485  3atlem2  39486  3atlem4  39488  3atlem5  39489  3atlem6  39490  3at  39492  islln3  39512  llnnleat  39515  llnn0  39518  llnle  39520  llnexatN  39523  llncmp  39524  2llnmat  39526  2at0mat0  39527  2atm  39529  ps-2c  39530  lplni2  39539  lplnle  39542  lplnnle2at  39543  lplnn0N  39549  islpln2a  39550  2atmat  39563  lplnexllnN  39566  2llnjaN  39568  2llnm4  39572  2llnmeqat  39573  lvoli3  39579  islvol5  39581  lvoli2  39583  lvolnle3at  39584  3atnelvolN  39588  lvoln0N  39593  islvol2aN  39594  4atlem3  39598  4atlem3a  39599  4atlem3b  39600  4atlem4a  39601  4atlem4b  39602  4atlem4c  39603  4atlem4d  39604  4atlem9  39605  4atlem10a  39606  4atlem10  39608  4atlem11a  39609  4atlem11b  39610  4atlem11  39611  4atlem12a  39612  4atlem12b  39613  4atlem12  39614  4at2  39616  lplncvrlvol2  39617  2lplnja  39621  dalempeb  39641  dalemqeb  39642  dalemreb  39643  dalemseb  39644  dalemteb  39645  dalemueb  39646  dalem3  39666  dalem16  39681  dalemcceb  39691  dalem21  39696  dalem25  39700  dalem38  39712  dalem39  39713  dalem43  39717  dalem44  39718  dalem45  39719  dalem53  39727  dalem54  39728  dalem55  39729  dalem57  39731  dalem60  39734  snatpsubN  39752  linepsubN  39754  pmaple  39763  pmapat  39765  pmap1N  39769  pmapsub  39770  pmapglbx  39771  isline2  39776  linepmap  39777  isline3  39778  isline4N  39779  lneq2at  39780  lncvrelatN  39783  lncmp  39785  2lnat  39786  2atm2atN  39787  2llnma1b  39788  2llnma1  39789  2llnma3r  39790  cdlema1N  39793  cdlemblem  39795  cdlemb  39796  elpaddn0  39802  paddcom  39815  paddasslem2  39823  paddasslem5  39826  paddasslem12  39833  paddasslem13  39834  pmapjoin  39854  pmapjat1  39855  pmapjat2  39856  pmapjlln1  39857  atmod1i1  39859  atmod1i2  39861  llnmod1i2  39862  atmod2i1  39863  atmod2i2  39864  atmod3i1  39866  atmod3i2  39867  atmod4i1  39868  atmod4i2  39869  llnexchb2lem  39870  llnexchb2  39871  dalawlem2  39874  dalawlem3  39875  dalawlem5  39877  dalawlem6  39878  dalawlem7  39879  dalawlem8  39880  dalawlem11  39883  dalawlem12  39884  polval2N  39908  pol1N  39912  polatN  39933  2polatN  39934  paddatclN  39951  linepsubclN  39953  lhp2lt  40003  lhp0lt  40005  lhpexle2lem  40011  lhpexle3lem  40013  lhpjat2  40023  lhpj1  40024  lhpmcvr3  40027  lhpmcvr4N  40028  lhpmcvr5N  40029  lhpmcvr6N  40030  lhpmatb  40033  lhp2at0  40034  lhp2atnle  40035  lhp2at0nle  40037  lhprelat3N  40042  lhple  40044  lhpat4N  40046  lhpat3  40048  4atexlemtlw  40069  4atexlemc  40071  4atexlemnclw  40072  4atexlemcnd  40074  4atex2-0aOLDN  40080  lauteq  40097  ltrnid  40137  ltrnel  40141  ltrnat  40142  ltrncnvat  40143  ltrncnvel  40144  ltrncoval  40147  ltrncnv  40148  ltrn11at  40149  ltrneq2  40150  ltrneq  40151  idltrn  40152  trlval2  40165  trlcnv  40167  trljat1  40168  trljat2  40169  ltrnideq  40177  arglem1N  40192  cdlemc1  40193  cdlemc2  40194  cdlemc4  40196  cdlemc5  40197  cdlemc6  40198  cdlemd1  40200  cdlemd2  40201  cdlemd3  40202  cdlemd4  40203  cdlemd7  40206  cdleme0aa  40212  cdleme0b  40214  cdleme0c  40215  cdleme0cp  40216  cdleme0cq  40217  cdleme0e  40219  cdleme0fN  40220  cdleme1b  40228  cdleme1  40229  cdleme2  40230  cdleme3b  40231  cdleme3c  40232  cdleme3e  40234  cdleme3g  40236  cdleme3h  40237  cdleme3  40239  cdleme5  40242  cdleme7d  40248  cdleme7e  40249  cdleme7ga  40250  cdleme7  40251  cdleme8  40252  cdleme9  40255  cdleme10  40256  cdleme11c  40263  cdleme11e  40265  cdleme11fN  40266  cdleme11g  40267  cdleme11k  40270  cdleme11  40272  cdleme15b  40277  cdleme15  40280  cdleme16b  40281  cdleme17b  40289  cdleme17c  40290  cdlemednpq  40301  cdleme20zN  40303  cdleme19a  40305  cdleme20bN  40312  cdleme20d  40314  cdleme20j  40320  cdleme21c  40329  cdleme22aa  40341  cdleme22b  40343  cdleme22cN  40344  cdleme22d  40345  cdleme22e  40346  cdleme22eALTN  40347  cdleme23b  40352  cdleme23c  40353  cdleme27N  40371  cdleme28a  40372  cdleme30a  40380  cdlemefrs29pre00  40397  cdlemefrs29bpre0  40398  cdlemefrs29cpre1  40400  cdlemefrs32fva  40402  cdlemefrs32fva1  40403  cdlemefr32snb  40407  cdlemefs32snb  40417  cdleme32snb  40438  cdleme32fva  40439  cdleme32fva1  40440  cdleme32fvaw  40441  cdleme35a  40450  cdleme35fnpq  40451  cdleme35b  40452  cdleme35c  40453  cdleme35f  40456  cdleme42c  40474  cdleme42e  40481  cdleme42h  40484  cdleme42i  40485  cdleme42ke  40487  cdleme42keg  40488  cdleme42mgN  40490  cdleme17d4  40499  cdleme48fvg  40502  cdleme48bw  40504  cdlemeg46req  40531  cdleme50trn3  40555  cdlemf1  40563  cdlemf2  40564  trlord  40571  ltrniotacnvval  40584  cdlemg2fv2  40602  cdlemg2l  40605  cdlemg7fvbwN  40609  cdlemg4c  40614  cdlemg4  40619  cdlemg6c  40622  cdlemg8b  40630  cdlemg11b  40644  cdlemg13a  40653  cdlemg17a  40663  cdlemg17h  40670  cdlemg17  40679  cdlemg18b  40681  cdlemg19a  40685  cdlemg27a  40694  cdlemg27b  40698  cdlemg31a  40699  cdlemg31b  40700  cdlemg31d  40702  cdlemg33b0  40703  cdlemg33a  40708  cdlemg35  40715  trlcolem  40728  cdlemg42  40731  cdlemg44a  40733  cdlemg46  40737  cdlemh1  40817  cdlemh2  40818  cdlemh  40819  cdlemi1  40820  cdlemi  40822  cdlemk3  40835  cdlemk4  40836  cdlemkvcl  40844  cdlemk7  40850  cdlemk11  40851  cdlemk15  40857  cdlemk1u  40861  cdlemk7u  40872  cdlemk11u  40873  cdlemk37  40916  cdlemk39  40918  cdlemkid1  40924  cdlemkid2  40926  cdlemk48  40952  cdlemk50  40954  cdlemk51  40955  cdlemk52  40956  dia2dimlem1  41066  dia2dimlem2  41067  dia2dimlem3  41068  dia2dimlem5  41070  dia2dimlem7  41072  dia2dimlem9  41074  dia2dimlem10  41075  dia2dimlem12  41077  dia2dimlem13  41078  cdlemm10N  41120  cdlemn2  41197  cdlemn3  41199  cdlemn9  41207  cdlemn10  41208  dihjustlem  41218  dihord1  41220  dihord2pre2  41228  dihvalcqat  41241  dib2dim  41245  dih2dimb  41246  dih2dimbALTN  41247  dihord5apre  41264  dihglbcpreN  41302  dihmeetlem3N  41307  dihmeetlem6  41311  dihjatc1  41313  dihjatc2N  41314  dihjatc3  41315  dihmeetlem9N  41317  dihmeetlem10N  41318  dihmeetlem11N  41319  dihmeetlem13N  41321  dihmeetlem15N  41323  dihmeetlem16N  41324  dihmeetlem17N  41325  dihatexv2  41341  dihjatb  41418  dihjatc  41419  dihjatcclem1  41420  dihjatcclem2  41421  dihjatcclem4  41423  dihjat  41425  dihjat3  41434  dihjat5N  41439  dvh4dimat  41440