Theorem atbase 39659

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3442  ∅c0 4287   class class class wbr 5100  ‘cfv 6500  Basecbs 17148  0.cp0 18356   ⋖ ccvr 39632  Atomscatm 39633

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 5243  ax-nul 5253  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508  df-ats 39637

This theorem is referenced by:  atssbase  39660  0ltat  39661  leatb  39662  meetat  39666  atnle0  39679  atlen0  39680  atcmp  39681  atcvreq0  39684  atncvrN  39685  atnle  39687  atnem0  39688  atlatmstc  39689  atlatle  39690  cvlexch2  39699  cvlexchb1  39700  cvlexchb2  39701  cvlatexchb1  39704  cvlatexchb2  39705  cvlatexch1  39706  cvlatexch2  39707  cvlatexch3  39708  cvlcvr1  39709  cvlcvrp  39710  cvlatcvr1  39711  cvlatcvr2  39712  cvlsupr2  39713  cvlsupr7  39718  cvlsupr8  39719  hlatjcl  39737  hlatjcom  39738  hlatjidm  39739  hlatjass  39740  hlatj32  39742  hlatj4  39744  hlatlej1  39745  atnlej1  39749  atnlej2  39750  hlrelat5N  39771  hlrelat  39772  hlrelat2  39773  exatleN  39774  cvr2N  39781  hlrelat3  39782  cvrval3  39783  cvrval5  39785  cvrexchlem  39789  cvratlem  39791  cvrat  39792  atcvr0eq  39796  lnnat  39797  cvrat2  39799  atcvrneN  39800  atcvrj1  39801  atcvrj2b  39802  atltcvr  39805  atle  39806  atlelt  39808  2atlt  39809  atexchcvrN  39810  cvrat3  39812  cvrat4  39813  cvrat42  39814  2atjm  39815  atbtwn  39816  3noncolr2  39819  4noncolr3  39823  athgt  39826  3dim0  39827  3dimlem3a  39830  3dimlem3OLDN  39832  3dimlem4a  39833  3dimlem4OLDN  39835  3dim3  39839  2dim  39840  1cvratex  39843  1cvrjat  39845  1cvrat  39846  ps-1  39847  ps-2  39848  hlatexch3N  39850  hlatexch4  39851  ps-2b  39852  3atlem1  39853  3atlem2  39854  3atlem4  39856  3atlem5  39857  3atlem6  39858  3at  39860  islln3  39880  llnnleat  39883  llnn0  39886  llnle  39888  llnexatN  39891  llncmp  39892  2llnmat  39894  2at0mat0  39895  2atm  39897  ps-2c  39898  lplni2  39907  lplnle  39910  lplnnle2at  39911  lplnn0N  39917  islpln2a  39918  2atmat  39931  lplnexllnN  39934  2llnjaN  39936  2llnm4  39940  2llnmeqat  39941  lvoli3  39947  islvol5  39949  lvoli2  39951  lvolnle3at  39952  3atnelvolN  39956  lvoln0N  39961  islvol2aN  39962  4atlem3  39966  4atlem3a  39967  4atlem3b  39968  4atlem4a  39969  4atlem4b  39970  4atlem4c  39971  4atlem4d  39972  4atlem9  39973  4atlem10a  39974  4atlem10  39976  4atlem11a  39977  4atlem11b  39978  4atlem11  39979  4atlem12a  39980  4atlem12b  39981  4atlem12  39982  4at2  39984  lplncvrlvol2  39985  2lplnja  39989  dalempeb  40009  dalemqeb  40010  dalemreb  40011  dalemseb  40012  dalemteb  40013  dalemueb  40014  dalem3  40034  dalem16  40049  dalemcceb  40059  dalem21  40064  dalem25  40068  dalem38  40080  dalem39  40081  dalem43  40085  dalem44  40086  dalem45  40087  dalem53  40095  dalem54  40096  dalem55  40097  dalem57  40099  dalem60  40102  snatpsubN  40120  linepsubN  40122  pmaple  40131  pmapat  40133  pmap1N  40137  pmapsub  40138  pmapglbx  40139  isline2  40144  linepmap  40145  isline3  40146  isline4N  40147  lneq2at  40148  lncvrelatN  40151  lncmp  40153  2lnat  40154  2atm2atN  40155  2llnma1b  40156  2llnma1  40157  2llnma3r  40158  cdlema1N  40161  cdlemblem  40163  cdlemb  40164  elpaddn0  40170  paddcom  40183  paddasslem2  40191  paddasslem5  40194  paddasslem12  40201  paddasslem13  40202  pmapjoin  40222  pmapjat1  40223  pmapjat2  40224  pmapjlln1  40225  atmod1i1  40227  atmod1i2  40229  llnmod1i2  40230  atmod2i1  40231  atmod2i2  40232  atmod3i1  40234  atmod3i2  40235  atmod4i1  40236  atmod4i2  40237  llnexchb2lem  40238  llnexchb2  40239  dalawlem2  40242  dalawlem3  40243  dalawlem5  40245  dalawlem6  40246  dalawlem7  40247  dalawlem8  40248  dalawlem11  40251  dalawlem12  40252  polval2N  40276  pol1N  40280  polatN  40301  2polatN  40302  paddatclN  40319  linepsubclN  40321  lhp2lt  40371  lhp0lt  40373  lhpexle2lem  40379  lhpexle3lem  40381  lhpjat2  40391  lhpj1  40392  lhpmcvr3  40395  lhpmcvr4N  40396  lhpmcvr5N  40397  lhpmcvr6N  40398  lhpmatb  40401  lhp2at0  40402  lhp2atnle  40403  lhp2at0nle  40405  lhprelat3N  40410  lhple  40412  lhpat4N  40414  lhpat3  40416  4atexlemtlw  40437  4atexlemc  40439  4atexlemnclw  40440  4atexlemcnd  40442  4atex2-0aOLDN  40448  lauteq  40465  ltrnid  40505  ltrnel  40509  ltrnat  40510  ltrncnvat  40511  ltrncnvel  40512  ltrncoval  40515  ltrncnv  40516  ltrn11at  40517  ltrneq2  40518  ltrneq  40519  idltrn  40520  trlval2  40533  trlcnv  40535  trljat1  40536  trljat2  40537  ltrnideq  40545  arglem1N  40560  cdlemc1  40561  cdlemc2  40562  cdlemc4  40564  cdlemc5  40565  cdlemc6  40566  cdlemd1  40568  cdlemd2  40569  cdlemd3  40570  cdlemd4  40571  cdlemd7  40574  cdleme0aa  40580  cdleme0b  40582  cdleme0c  40583  cdleme0cp  40584  cdleme0cq  40585  cdleme0e  40587  cdleme0fN  40588  cdleme1b  40596  cdleme1  40597  cdleme2  40598  cdleme3b  40599  cdleme3c  40600  cdleme3e  40602  cdleme3g  40604  cdleme3h  40605  cdleme3  40607  cdleme5  40610  cdleme7d  40616  cdleme7e  40617  cdleme7ga  40618  cdleme7  40619  cdleme8  40620  cdleme9  40623  cdleme10  40624  cdleme11c  40631  cdleme11e  40633  cdleme11fN  40634  cdleme11g  40635  cdleme11k  40638  cdleme11  40640  cdleme15b  40645  cdleme15  40648  cdleme16b  40649  cdleme17b  40657  cdleme17c  40658  cdlemednpq  40669  cdleme20zN  40671  cdleme19a  40673  cdleme20bN  40680  cdleme20d  40682  cdleme20j  40688  cdleme21c  40697  cdleme22aa  40709  cdleme22b  40711  cdleme22cN  40712  cdleme22d  40713  cdleme22e  40714  cdleme22eALTN  40715  cdleme23b  40720  cdleme23c  40721  cdleme27N  40739  cdleme28a  40740  cdleme30a  40748  cdlemefrs29pre00  40765  cdlemefrs29bpre0  40766  cdlemefrs29cpre1  40768  cdlemefrs32fva  40770  cdlemefrs32fva1  40771  cdlemefr32snb  40775  cdlemefs32snb  40785  cdleme32snb  40806  cdleme32fva  40807  cdleme32fva1  40808  cdleme32fvaw  40809  cdleme35a  40818  cdleme35fnpq  40819  cdleme35b  40820  cdleme35c  40821  cdleme35f  40824  cdleme42c  40842  cdleme42e  40849  cdleme42h  40852  cdleme42i  40853  cdleme42ke  40855  cdleme42keg  40856  cdleme42mgN  40858  cdleme17d4  40867  cdleme48fvg  40870  cdleme48bw  40872  cdlemeg46req  40899  cdleme50trn3  40923  cdlemf1  40931  cdlemf2  40932  trlord  40939  ltrniotacnvval  40952  cdlemg2fv2  40970  cdlemg2l  40973  cdlemg7fvbwN  40977  cdlemg4c  40982  cdlemg4  40987  cdlemg6c  40990  cdlemg8b  40998  cdlemg11b  41012  cdlemg13a  41021  cdlemg17a  41031  cdlemg17h  41038  cdlemg17  41047  cdlemg18b  41049  cdlemg19a  41053  cdlemg27a  41062  cdlemg27b  41066  cdlemg31a  41067  cdlemg31b  41068  cdlemg31d  41070  cdlemg33b0  41071  cdlemg33a  41076  cdlemg35  41083  trlcolem  41096  cdlemg42  41099  cdlemg44a  41101  cdlemg46  41105  cdlemh1  41185  cdlemh2  41186  cdlemh  41187  cdlemi1  41188  cdlemi  41190  cdlemk3  41203  cdlemk4  41204  cdlemkvcl  41212  cdlemk7  41218  cdlemk11  41219  cdlemk15  41225  cdlemk1u  41229  cdlemk7u  41240  cdlemk11u  41241  cdlemk37  41284  cdlemk39  41286  cdlemkid1  41292  cdlemkid2  41294  cdlemk48  41320  cdlemk50  41322  cdlemk51  41323  cdlemk52  41324  dia2dimlem1  41434  dia2dimlem2  41435  dia2dimlem3  41436  dia2dimlem5  41438  dia2dimlem7  41440  dia2dimlem9  41442  dia2dimlem10  41443  dia2dimlem12  41445  dia2dimlem13  41446  cdlemm10N  41488  cdlemn2  41565  cdlemn3  41567  cdlemn9  41575  cdlemn10  41576  dihjustlem  41586  dihord1  41588  dihord2pre2  41596  dihvalcqat  41609  dib2dim  41613  dih2dimb  41614  dih2dimbALTN  41615  dihord5apre  41632  dihglbcpreN  41670  dihmeetlem3N  41675  dihmeetlem6  41679  dihjatc1  41681  dihjatc2N  41682  dihjatc3  41683  dihmeetlem9N  41685  dihmeetlem10N  41686  dihmeetlem11N  41687  dihmeetlem13N  41689  dihmeetlem15N  41691  dihmeetlem16N  41692  dihmeetlem17N  41693  dihatexv2  41709  dihjatb  41786  dihjatc  41787  dihjatcclem1  41788  dihjatcclem2  41789  dihjatcclem4  41791  dihjat  41793  dihjat3  41802  dihjat5N  41807  dvh4dimat  41808