Theorem atbase 39749

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 32430 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 4281	. . . 4 ⊢ (𝑃 ∈ 𝐴 → ¬ 𝐴 = ∅)
2		atombase.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
3	2	eqeq1i 2742	. . . 4 ⊢ (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
4	1, 3	sylnib 328	. . 3 ⊢ (𝑃 ∈ 𝐴 → ¬ (Atoms‘𝐾) = ∅)
5		fvprc 6826	. . 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 39746	. . 3 ⊢ (𝐾 ∈ V → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
11	10	simprbda 498	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐵)
12	6, 11	mpancom 689	1 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3430  ∅c0 4274   class class class wbr 5086  ‘cfv 6492  Basecbs 17170  0.cp0 18378   ⋖ ccvr 39722  Atomscatm 39723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-ats 39727

This theorem is referenced by:  atssbase  39750  0ltat  39751  leatb  39752  meetat  39756  atnle0  39769  atlen0  39770  atcmp  39771  atcvreq0  39774  atncvrN  39775  atnle  39777  atnem0  39778  atlatmstc  39779  atlatle  39780  cvlexch2  39789  cvlexchb1  39790  cvlexchb2  39791  cvlatexchb1  39794  cvlatexchb2  39795  cvlatexch1  39796  cvlatexch2  39797  cvlatexch3  39798  cvlcvr1  39799  cvlcvrp  39800  cvlatcvr1  39801  cvlatcvr2  39802  cvlsupr2  39803  cvlsupr7  39808  cvlsupr8  39809  hlatjcl  39827  hlatjcom  39828  hlatjidm  39829  hlatjass  39830  hlatj32  39832  hlatj4  39834  hlatlej1  39835  atnlej1  39839  atnlej2  39840  hlrelat5N  39861  hlrelat  39862  hlrelat2  39863  exatleN  39864  cvr2N  39871  hlrelat3  39872  cvrval3  39873  cvrval5  39875  cvrexchlem  39879  cvratlem  39881  cvrat  39882  atcvr0eq  39886  lnnat  39887  cvrat2  39889  atcvrneN  39890  atcvrj1  39891  atcvrj2b  39892  atltcvr  39895  atle  39896  atlelt  39898  2atlt  39899  atexchcvrN  39900  cvrat3  39902  cvrat4  39903  cvrat42  39904  2atjm  39905  atbtwn  39906  3noncolr2  39909  4noncolr3  39913  athgt  39916  3dim0  39917  3dimlem3a  39920  3dimlem3OLDN  39922  3dimlem4a  39923  3dimlem4OLDN  39925  3dim3  39929  2dim  39930  1cvratex  39933  1cvrjat  39935  1cvrat  39936  ps-1  39937  ps-2  39938  hlatexch3N  39940  hlatexch4  39941  ps-2b  39942  3atlem1  39943  3atlem2  39944  3atlem4  39946  3atlem5  39947  3atlem6  39948  3at  39950  islln3  39970  llnnleat  39973  llnn0  39976  llnle  39978  llnexatN  39981  llncmp  39982  2llnmat  39984  2at0mat0  39985  2atm  39987  ps-2c  39988  lplni2  39997  lplnle  40000  lplnnle2at  40001  lplnn0N  40007  islpln2a  40008  2atmat  40021  lplnexllnN  40024  2llnjaN  40026  2llnm4  40030  2llnmeqat  40031  lvoli3  40037  islvol5  40039  lvoli2  40041  lvolnle3at  40042  3atnelvolN  40046  lvoln0N  40051  islvol2aN  40052  4atlem3  40056  4atlem3a  40057  4atlem3b  40058  4atlem4a  40059  4atlem4b  40060  4atlem4c  40061  4atlem4d  40062  4atlem9  40063  4atlem10a  40064  4atlem10  40066  4atlem11a  40067  4atlem11b  40068  4atlem11  40069  4atlem12a  40070  4atlem12b  40071  4atlem12  40072  4at2  40074  lplncvrlvol2  40075  2lplnja  40079  dalempeb  40099  dalemqeb  40100  dalemreb  40101  dalemseb  40102  dalemteb  40103  dalemueb  40104  dalem3  40124  dalem16  40139  dalemcceb  40149  dalem21  40154  dalem25  40158  dalem38  40170  dalem39  40171  dalem43  40175  dalem44  40176  dalem45  40177  dalem53  40185  dalem54  40186  dalem55  40187  dalem57  40189  dalem60  40192  snatpsubN  40210  linepsubN  40212  pmaple  40221  pmapat  40223  pmap1N  40227  pmapsub  40228  pmapglbx  40229  isline2  40234  linepmap  40235  isline3  40236  isline4N  40237  lneq2at  40238  lncvrelatN  40241  lncmp  40243  2lnat  40244  2atm2atN  40245  2llnma1b  40246  2llnma1  40247  2llnma3r  40248  cdlema1N  40251  cdlemblem  40253  cdlemb  40254  elpaddn0  40260  paddcom  40273  paddasslem2  40281  paddasslem5  40284  paddasslem12  40291  paddasslem13  40292  pmapjoin  40312  pmapjat1  40313  pmapjat2  40314  pmapjlln1  40315  atmod1i1  40317  atmod1i2  40319  llnmod1i2  40320  atmod2i1  40321  atmod2i2  40322  atmod3i1  40324  atmod3i2  40325  atmod4i1  40326  atmod4i2  40327  llnexchb2lem  40328  llnexchb2  40329  dalawlem2  40332  dalawlem3  40333  dalawlem5  40335  dalawlem6  40336  dalawlem7  40337  dalawlem8  40338  dalawlem11  40341  dalawlem12  40342  polval2N  40366  pol1N  40370  polatN  40391  2polatN  40392  paddatclN  40409  linepsubclN  40411  lhp2lt  40461  lhp0lt  40463  lhpexle2lem  40469  lhpexle3lem  40471  lhpjat2  40481  lhpj1  40482  lhpmcvr3  40485  lhpmcvr4N  40486  lhpmcvr5N  40487  lhpmcvr6N  40488  lhpmatb  40491  lhp2at0  40492  lhp2atnle  40493  lhp2at0nle  40495  lhprelat3N  40500  lhple  40502  lhpat4N  40504  lhpat3  40506  4atexlemtlw  40527  4atexlemc  40529  4atexlemnclw  40530  4atexlemcnd  40532  4atex2-0aOLDN  40538  lauteq  40555  ltrnid  40595  ltrnel  40599  ltrnat  40600  ltrncnvat  40601  ltrncnvel  40602  ltrncoval  40605  ltrncnv  40606  ltrn11at  40607  ltrneq2  40608  ltrneq  40609  idltrn  40610  trlval2  40623  trlcnv  40625  trljat1  40626  trljat2  40627  ltrnideq  40635  arglem1N  40650  cdlemc1  40651  cdlemc2  40652  cdlemc4  40654  cdlemc5  40655  cdlemc6  40656  cdlemd1  40658  cdlemd2  40659  cdlemd3  40660  cdlemd4  40661  cdlemd7  40664  cdleme0aa  40670  cdleme0b  40672  cdleme0c  40673  cdleme0cp  40674  cdleme0cq  40675  cdleme0e  40677  cdleme0fN  40678  cdleme1b  40686  cdleme1  40687  cdleme2  40688  cdleme3b  40689  cdleme3c  40690  cdleme3e  40692  cdleme3g  40694  cdleme3h  40695  cdleme3  40697  cdleme5  40700  cdleme7d  40706  cdleme7e  40707  cdleme7ga  40708  cdleme7  40709  cdleme8  40710  cdleme9  40713  cdleme10  40714  cdleme11c  40721  cdleme11e  40723  cdleme11fN  40724  cdleme11g  40725  cdleme11k  40728  cdleme11  40730  cdleme15b  40735  cdleme15  40738  cdleme16b  40739  cdleme17b  40747  cdleme17c  40748  cdlemednpq  40759  cdleme20zN  40761  cdleme19a  40763  cdleme20bN  40770  cdleme20d  40772  cdleme20j  40778  cdleme21c  40787  cdleme22aa  40799  cdleme22b  40801  cdleme22cN  40802  cdleme22d  40803  cdleme22e  40804  cdleme22eALTN  40805  cdleme23b  40810  cdleme23c  40811  cdleme27N  40829  cdleme28a  40830  cdleme30a  40838  cdlemefrs29pre00  40855  cdlemefrs29bpre0  40856  cdlemefrs29cpre1  40858  cdlemefrs32fva  40860  cdlemefrs32fva1  40861  cdlemefr32snb  40865  cdlemefs32snb  40875  cdleme32snb  40896  cdleme32fva  40897  cdleme32fva1  40898  cdleme32fvaw  40899  cdleme35a  40908  cdleme35fnpq  40909  cdleme35b  40910  cdleme35c  40911  cdleme35f  40914  cdleme42c  40932  cdleme42e  40939  cdleme42h  40942  cdleme42i  40943  cdleme42ke  40945  cdleme42keg  40946  cdleme42mgN  40948  cdleme17d4  40957  cdleme48fvg  40960  cdleme48bw  40962  cdlemeg46req  40989  cdleme50trn3  41013  cdlemf1  41021  cdlemf2  41022  trlord  41029  ltrniotacnvval  41042  cdlemg2fv2  41060  cdlemg2l  41063  cdlemg7fvbwN  41067  cdlemg4c  41072  cdlemg4  41077  cdlemg6c  41080  cdlemg8b  41088  cdlemg11b  41102  cdlemg13a  41111  cdlemg17a  41121  cdlemg17h  41128  cdlemg17  41137  cdlemg18b  41139  cdlemg19a  41143  cdlemg27a  41152  cdlemg27b  41156  cdlemg31a  41157  cdlemg31b  41158  cdlemg31d  41160  cdlemg33b0  41161  cdlemg33a  41166  cdlemg35  41173  trlcolem  41186  cdlemg42  41189  cdlemg44a  41191  cdlemg46  41195  cdlemh1  41275  cdlemh2  41276  cdlemh  41277  cdlemi1  41278  cdlemi  41280  cdlemk3  41293  cdlemk4  41294  cdlemkvcl  41302  cdlemk7  41308  cdlemk11  41309  cdlemk15  41315  cdlemk1u  41319  cdlemk7u  41330  cdlemk11u  41331  cdlemk37  41374  cdlemk39  41376  cdlemkid1  41382  cdlemkid2  41384  cdlemk48  41410  cdlemk50  41412  cdlemk51  41413  cdlemk52  41414  dia2dimlem1  41524  dia2dimlem2  41525  dia2dimlem3  41526  dia2dimlem5  41528  dia2dimlem7  41530  dia2dimlem9  41532  dia2dimlem10  41533  dia2dimlem12  41535  dia2dimlem13  41536  cdlemm10N  41578  cdlemn2  41655  cdlemn3  41657  cdlemn9  41665  cdlemn10  41666  dihjustlem  41676  dihord1  41678  dihord2pre2  41686  dihvalcqat  41699  dib2dim  41703  dih2dimb  41704  dih2dimbALTN  41705  dihord5apre  41722  dihglbcpreN  41760  dihmeetlem3N  41765  dihmeetlem6  41769  dihjatc1  41771  dihjatc2N  41772  dihjatc3  41773  dihmeetlem9N  41775  dihmeetlem10N  41776  dihmeetlem11N  41777  dihmeetlem13N  41779  dihmeetlem15N  41781  dihmeetlem16N  41782  dihmeetlem17N  41783  dihatexv2  41799  dihjatb  41876  dihjatc  41877  dihjatcclem1  41878  dihjatcclem2  41879  dihjatcclem4  41881  dihjat  41883  dihjat3  41892  dihjat5N  41897  dvh4dimat  41898