Theorem atbase 39282

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3447  ∅c0 4296   class class class wbr 5107  ‘cfv 6511  Basecbs 17179  0.cp0 18382   ⋖ ccvr 39255  Atomscatm 39256

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519  df-ats 39260

This theorem is referenced by:  atssbase  39283  0ltat  39284  leatb  39285  meetat  39289  atnle0  39302  atlen0  39303  atcmp  39304  atcvreq0  39307  atncvrN  39308  atnle  39310  atnem0  39311  atlatmstc  39312  atlatle  39313  cvlexch2  39322  cvlexchb1  39323  cvlexchb2  39324  cvlatexchb1  39327  cvlatexchb2  39328  cvlatexch1  39329  cvlatexch2  39330  cvlatexch3  39331  cvlcvr1  39332  cvlcvrp  39333  cvlatcvr1  39334  cvlatcvr2  39335  cvlsupr2  39336  cvlsupr7  39341  cvlsupr8  39342  hlatjcl  39360  hlatjcom  39361  hlatjidm  39362  hlatjass  39363  hlatj32  39365  hlatj4  39367  hlatlej1  39368  atnlej1  39373  atnlej2  39374  hlrelat5N  39395  hlrelat  39396  hlrelat2  39397  exatleN  39398  cvr2N  39405  hlrelat3  39406  cvrval3  39407  cvrval5  39409  cvrexchlem  39413  cvratlem  39415  cvrat  39416  atcvr0eq  39420  lnnat  39421  cvrat2  39423  atcvrneN  39424  atcvrj1  39425  atcvrj2b  39426  atltcvr  39429  atle  39430  atlelt  39432  2atlt  39433  atexchcvrN  39434  cvrat3  39436  cvrat4  39437  cvrat42  39438  2atjm  39439  atbtwn  39440  3noncolr2  39443  4noncolr3  39447  athgt  39450  3dim0  39451  3dimlem3a  39454  3dimlem3OLDN  39456  3dimlem4a  39457  3dimlem4OLDN  39459  3dim3  39463  2dim  39464  1cvratex  39467  1cvrjat  39469  1cvrat  39470  ps-1  39471  ps-2  39472  hlatexch3N  39474  hlatexch4  39475  ps-2b  39476  3atlem1  39477  3atlem2  39478  3atlem4  39480  3atlem5  39481  3atlem6  39482  3at  39484  islln3  39504  llnnleat  39507  llnn0  39510  llnle  39512  llnexatN  39515  llncmp  39516  2llnmat  39518  2at0mat0  39519  2atm  39521  ps-2c  39522  lplni2  39531  lplnle  39534  lplnnle2at  39535  lplnn0N  39541  islpln2a  39542  2atmat  39555  lplnexllnN  39558  2llnjaN  39560  2llnm4  39564  2llnmeqat  39565  lvoli3  39571  islvol5  39573  lvoli2  39575  lvolnle3at  39576  3atnelvolN  39580  lvoln0N  39585  islvol2aN  39586  4atlem3  39590  4atlem3a  39591  4atlem3b  39592  4atlem4a  39593  4atlem4b  39594  4atlem4c  39595  4atlem4d  39596  4atlem9  39597  4atlem10a  39598  4atlem10  39600  4atlem11a  39601  4atlem11b  39602  4atlem11  39603  4atlem12a  39604  4atlem12b  39605  4atlem12  39606  4at2  39608  lplncvrlvol2  39609  2lplnja  39613  dalempeb  39633  dalemqeb  39634  dalemreb  39635  dalemseb  39636  dalemteb  39637  dalemueb  39638  dalem3  39658  dalem16  39673  dalemcceb  39683  dalem21  39688  dalem25  39692  dalem38  39704  dalem39  39705  dalem43  39709  dalem44  39710  dalem45  39711  dalem53  39719  dalem54  39720  dalem55  39721  dalem57  39723  dalem60  39726  snatpsubN  39744  linepsubN  39746  pmaple  39755  pmapat  39757  pmap1N  39761  pmapsub  39762  pmapglbx  39763  isline2  39768  linepmap  39769  isline3  39770  isline4N  39771  lneq2at  39772  lncvrelatN  39775  lncmp  39777  2lnat  39778  2atm2atN  39779  2llnma1b  39780  2llnma1  39781  2llnma3r  39782  cdlema1N  39785  cdlemblem  39787  cdlemb  39788  elpaddn0  39794  paddcom  39807  paddasslem2  39815  paddasslem5  39818  paddasslem12  39825  paddasslem13  39826  pmapjoin  39846  pmapjat1  39847  pmapjat2  39848  pmapjlln1  39849  atmod1i1  39851  atmod1i2  39853  llnmod1i2  39854  atmod2i1  39855  atmod2i2  39856  atmod3i1  39858  atmod3i2  39859  atmod4i1  39860  atmod4i2  39861  llnexchb2lem  39862  llnexchb2  39863  dalawlem2  39866  dalawlem3  39867  dalawlem5  39869  dalawlem6  39870  dalawlem7  39871  dalawlem8  39872  dalawlem11  39875  dalawlem12  39876  polval2N  39900  pol1N  39904  polatN  39925  2polatN  39926  paddatclN  39943  linepsubclN  39945  lhp2lt  39995  lhp0lt  39997  lhpexle2lem  40003  lhpexle3lem  40005  lhpjat2  40015  lhpj1  40016  lhpmcvr3  40019  lhpmcvr4N  40020  lhpmcvr5N  40021  lhpmcvr6N  40022  lhpmatb  40025  lhp2at0  40026  lhp2atnle  40027  lhp2at0nle  40029  lhprelat3N  40034  lhple  40036  lhpat4N  40038  lhpat3  40040  4atexlemtlw  40061  4atexlemc  40063  4atexlemnclw  40064  4atexlemcnd  40066  4atex2-0aOLDN  40072  lauteq  40089  ltrnid  40129  ltrnel  40133  ltrnat  40134  ltrncnvat  40135  ltrncnvel  40136  ltrncoval  40139  ltrncnv  40140  ltrn11at  40141  ltrneq2  40142  ltrneq  40143  idltrn  40144  trlval2  40157  trlcnv  40159  trljat1  40160  trljat2  40161  ltrnideq  40169  arglem1N  40184  cdlemc1  40185  cdlemc2  40186  cdlemc4  40188  cdlemc5  40189  cdlemc6  40190  cdlemd1  40192  cdlemd2  40193  cdlemd3  40194  cdlemd4  40195  cdlemd7  40198  cdleme0aa  40204  cdleme0b  40206  cdleme0c  40207  cdleme0cp  40208  cdleme0cq  40209  cdleme0e  40211  cdleme0fN  40212  cdleme1b  40220  cdleme1  40221  cdleme2  40222  cdleme3b  40223  cdleme3c  40224  cdleme3e  40226  cdleme3g  40228  cdleme3h  40229  cdleme3  40231  cdleme5  40234  cdleme7d  40240  cdleme7e  40241  cdleme7ga  40242  cdleme7  40243  cdleme8  40244  cdleme9  40247  cdleme10  40248  cdleme11c  40255  cdleme11e  40257  cdleme11fN  40258  cdleme11g  40259  cdleme11k  40262  cdleme11  40264  cdleme15b  40269  cdleme15  40272  cdleme16b  40273  cdleme17b  40281  cdleme17c  40282  cdlemednpq  40293  cdleme20zN  40295  cdleme19a  40297  cdleme20bN  40304  cdleme20d  40306  cdleme20j  40312  cdleme21c  40321  cdleme22aa  40333  cdleme22b  40335  cdleme22cN  40336  cdleme22d  40337  cdleme22e  40338  cdleme22eALTN  40339  cdleme23b  40344  cdleme23c  40345  cdleme27N  40363  cdleme28a  40364  cdleme30a  40372  cdlemefrs29pre00  40389  cdlemefrs29bpre0  40390  cdlemefrs29cpre1  40392  cdlemefrs32fva  40394  cdlemefrs32fva1  40395  cdlemefr32snb  40399  cdlemefs32snb  40409  cdleme32snb  40430  cdleme32fva  40431  cdleme32fva1  40432  cdleme32fvaw  40433  cdleme35a  40442  cdleme35fnpq  40443  cdleme35b  40444  cdleme35c  40445  cdleme35f  40448  cdleme42c  40466  cdleme42e  40473  cdleme42h  40476  cdleme42i  40477  cdleme42ke  40479  cdleme42keg  40480  cdleme42mgN  40482  cdleme17d4  40491  cdleme48fvg  40494  cdleme48bw  40496  cdlemeg46req  40523  cdleme50trn3  40547  cdlemf1  40555  cdlemf2  40556  trlord  40563  ltrniotacnvval  40576  cdlemg2fv2  40594  cdlemg2l  40597  cdlemg7fvbwN  40601  cdlemg4c  40606  cdlemg4  40611  cdlemg6c  40614  cdlemg8b  40622  cdlemg11b  40636  cdlemg13a  40645  cdlemg17a  40655  cdlemg17h  40662  cdlemg17  40671  cdlemg18b  40673  cdlemg19a  40677  cdlemg27a  40686  cdlemg27b  40690  cdlemg31a  40691  cdlemg31b  40692  cdlemg31d  40694  cdlemg33b0  40695  cdlemg33a  40700  cdlemg35  40707  trlcolem  40720  cdlemg42  40723  cdlemg44a  40725  cdlemg46  40729  cdlemh1  40809  cdlemh2  40810  cdlemh  40811  cdlemi1  40812  cdlemi  40814  cdlemk3  40827  cdlemk4  40828  cdlemkvcl  40836  cdlemk7  40842  cdlemk11  40843  cdlemk15  40849  cdlemk1u  40853  cdlemk7u  40864  cdlemk11u  40865  cdlemk37  40908  cdlemk39  40910  cdlemkid1  40916  cdlemkid2  40918  cdlemk48  40944  cdlemk50  40946  cdlemk51  40947  cdlemk52  40948  dia2dimlem1  41058  dia2dimlem2  41059  dia2dimlem3  41060  dia2dimlem5  41062  dia2dimlem7  41064  dia2dimlem9  41066  dia2dimlem10  41067  dia2dimlem12  41069  dia2dimlem13  41070  cdlemm10N  41112  cdlemn2  41189  cdlemn3  41191  cdlemn9  41199  cdlemn10  41200  dihjustlem  41210  dihord1  41212  dihord2pre2  41220  dihvalcqat  41233  dib2dim  41237  dih2dimb  41238  dih2dimbALTN  41239  dihord5apre  41256  dihglbcpreN  41294  dihmeetlem3N  41299  dihmeetlem6  41303  dihjatc1  41305  dihjatc2N  41306  dihjatc3  41307  dihmeetlem9N  41309  dihmeetlem10N  41310  dihmeetlem11N  41311  dihmeetlem13N  41313  dihmeetlem15N  41315  dihmeetlem16N  41316  dihmeetlem17N  41317  dihatexv2  41333  dihjatb  41410  dihjatc  41411  dihjatcclem1  41412  dihjatcclem2  41413  dihjatcclem4  41415  dihjat  41417  dihjat3  41426  dihjat5N  41431  dvh4dimat  41432