Theorem atbase 39545

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 32419 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 4292	. . . 4 ⊢ (𝑃 ∈ 𝐴 → ¬ 𝐴 = ∅)
2		atombase.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
3	2	eqeq1i 2741	. . . 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 2736	. . . 4 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		eqid 2736	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	isat 39542	. . 3 ⊢ (𝐾 ∈ V → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
11	10	simprbda 498	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐵)
12	6, 11	mpancom 688	1 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3440  ∅c0 4285   class class class wbr 5098  ‘cfv 6492  Basecbs 17136  0.cp0 18344   ⋖ ccvr 39518  Atomscatm 39519

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 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  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 39523

This theorem is referenced by:  atssbase  39546  0ltat  39547  leatb  39548  meetat  39552  atnle0  39565  atlen0  39566  atcmp  39567  atcvreq0  39570  atncvrN  39571  atnle  39573  atnem0  39574  atlatmstc  39575  atlatle  39576  cvlexch2  39585  cvlexchb1  39586  cvlexchb2  39587  cvlatexchb1  39590  cvlatexchb2  39591  cvlatexch1  39592  cvlatexch2  39593  cvlatexch3  39594  cvlcvr1  39595  cvlcvrp  39596  cvlatcvr1  39597  cvlatcvr2  39598  cvlsupr2  39599  cvlsupr7  39604  cvlsupr8  39605  hlatjcl  39623  hlatjcom  39624  hlatjidm  39625  hlatjass  39626  hlatj32  39628  hlatj4  39630  hlatlej1  39631  atnlej1  39635  atnlej2  39636  hlrelat5N  39657  hlrelat  39658  hlrelat2  39659  exatleN  39660  cvr2N  39667  hlrelat3  39668  cvrval3  39669  cvrval5  39671  cvrexchlem  39675  cvratlem  39677  cvrat  39678  atcvr0eq  39682  lnnat  39683  cvrat2  39685  atcvrneN  39686  atcvrj1  39687  atcvrj2b  39688  atltcvr  39691  atle  39692  atlelt  39694  2atlt  39695  atexchcvrN  39696  cvrat3  39698  cvrat4  39699  cvrat42  39700  2atjm  39701  atbtwn  39702  3noncolr2  39705  4noncolr3  39709  athgt  39712  3dim0  39713  3dimlem3a  39716  3dimlem3OLDN  39718  3dimlem4a  39719  3dimlem4OLDN  39721  3dim3  39725  2dim  39726  1cvratex  39729  1cvrjat  39731  1cvrat  39732  ps-1  39733  ps-2  39734  hlatexch3N  39736  hlatexch4  39737  ps-2b  39738  3atlem1  39739  3atlem2  39740  3atlem4  39742  3atlem5  39743  3atlem6  39744  3at  39746  islln3  39766  llnnleat  39769  llnn0  39772  llnle  39774  llnexatN  39777  llncmp  39778  2llnmat  39780  2at0mat0  39781  2atm  39783  ps-2c  39784  lplni2  39793  lplnle  39796  lplnnle2at  39797  lplnn0N  39803  islpln2a  39804  2atmat  39817  lplnexllnN  39820  2llnjaN  39822  2llnm4  39826  2llnmeqat  39827  lvoli3  39833  islvol5  39835  lvoli2  39837  lvolnle3at  39838  3atnelvolN  39842  lvoln0N  39847  islvol2aN  39848  4atlem3  39852  4atlem3a  39853  4atlem3b  39854  4atlem4a  39855  4atlem4b  39856  4atlem4c  39857  4atlem4d  39858  4atlem9  39859  4atlem10a  39860  4atlem10  39862  4atlem11a  39863  4atlem11b  39864  4atlem11  39865  4atlem12a  39866  4atlem12b  39867  4atlem12  39868  4at2  39870  lplncvrlvol2  39871  2lplnja  39875  dalempeb  39895  dalemqeb  39896  dalemreb  39897  dalemseb  39898  dalemteb  39899  dalemueb  39900  dalem3  39920  dalem16  39935  dalemcceb  39945  dalem21  39950  dalem25  39954  dalem38  39966  dalem39  39967  dalem43  39971  dalem44  39972  dalem45  39973  dalem53  39981  dalem54  39982  dalem55  39983  dalem57  39985  dalem60  39988  snatpsubN  40006  linepsubN  40008  pmaple  40017  pmapat  40019  pmap1N  40023  pmapsub  40024  pmapglbx  40025  isline2  40030  linepmap  40031  isline3  40032  isline4N  40033  lneq2at  40034  lncvrelatN  40037  lncmp  40039  2lnat  40040  2atm2atN  40041  2llnma1b  40042  2llnma1  40043  2llnma3r  40044  cdlema1N  40047  cdlemblem  40049  cdlemb  40050  elpaddn0  40056  paddcom  40069  paddasslem2  40077  paddasslem5  40080  paddasslem12  40087  paddasslem13  40088  pmapjoin  40108  pmapjat1  40109  pmapjat2  40110  pmapjlln1  40111  atmod1i1  40113  atmod1i2  40115  llnmod1i2  40116  atmod2i1  40117  atmod2i2  40118  atmod3i1  40120  atmod3i2  40121  atmod4i1  40122  atmod4i2  40123  llnexchb2lem  40124  llnexchb2  40125  dalawlem2  40128  dalawlem3  40129  dalawlem5  40131  dalawlem6  40132  dalawlem7  40133  dalawlem8  40134  dalawlem11  40137  dalawlem12  40138  polval2N  40162  pol1N  40166  polatN  40187  2polatN  40188  paddatclN  40205  linepsubclN  40207  lhp2lt  40257  lhp0lt  40259  lhpexle2lem  40265  lhpexle3lem  40267  lhpjat2  40277  lhpj1  40278  lhpmcvr3  40281  lhpmcvr4N  40282  lhpmcvr5N  40283  lhpmcvr6N  40284  lhpmatb  40287  lhp2at0  40288  lhp2atnle  40289  lhp2at0nle  40291  lhprelat3N  40296  lhple  40298  lhpat4N  40300  lhpat3  40302  4atexlemtlw  40323  4atexlemc  40325  4atexlemnclw  40326  4atexlemcnd  40328  4atex2-0aOLDN  40334  lauteq  40351  ltrnid  40391  ltrnel  40395  ltrnat  40396  ltrncnvat  40397  ltrncnvel  40398  ltrncoval  40401  ltrncnv  40402  ltrn11at  40403  ltrneq2  40404  ltrneq  40405  idltrn  40406  trlval2  40419  trlcnv  40421  trljat1  40422  trljat2  40423  ltrnideq  40431  arglem1N  40446  cdlemc1  40447  cdlemc2  40448  cdlemc4  40450  cdlemc5  40451  cdlemc6  40452  cdlemd1  40454  cdlemd2  40455  cdlemd3  40456  cdlemd4  40457  cdlemd7  40460  cdleme0aa  40466  cdleme0b  40468  cdleme0c  40469  cdleme0cp  40470  cdleme0cq  40471  cdleme0e  40473  cdleme0fN  40474  cdleme1b  40482  cdleme1  40483  cdleme2  40484  cdleme3b  40485  cdleme3c  40486  cdleme3e  40488  cdleme3g  40490  cdleme3h  40491  cdleme3  40493  cdleme5  40496  cdleme7d  40502  cdleme7e  40503  cdleme7ga  40504  cdleme7  40505  cdleme8  40506  cdleme9  40509  cdleme10  40510  cdleme11c  40517  cdleme11e  40519  cdleme11fN  40520  cdleme11g  40521  cdleme11k  40524  cdleme11  40526  cdleme15b  40531  cdleme15  40534  cdleme16b  40535  cdleme17b  40543  cdleme17c  40544  cdlemednpq  40555  cdleme20zN  40557  cdleme19a  40559  cdleme20bN  40566  cdleme20d  40568  cdleme20j  40574  cdleme21c  40583  cdleme22aa  40595  cdleme22b  40597  cdleme22cN  40598  cdleme22d  40599  cdleme22e  40600  cdleme22eALTN  40601  cdleme23b  40606  cdleme23c  40607  cdleme27N  40625  cdleme28a  40626  cdleme30a  40634  cdlemefrs29pre00  40651  cdlemefrs29bpre0  40652  cdlemefrs29cpre1  40654  cdlemefrs32fva  40656  cdlemefrs32fva1  40657  cdlemefr32snb  40661  cdlemefs32snb  40671  cdleme32snb  40692  cdleme32fva  40693  cdleme32fva1  40694  cdleme32fvaw  40695  cdleme35a  40704  cdleme35fnpq  40705  cdleme35b  40706  cdleme35c  40707  cdleme35f  40710  cdleme42c  40728  cdleme42e  40735  cdleme42h  40738  cdleme42i  40739  cdleme42ke  40741  cdleme42keg  40742  cdleme42mgN  40744  cdleme17d4  40753  cdleme48fvg  40756  cdleme48bw  40758  cdlemeg46req  40785  cdleme50trn3  40809  cdlemf1  40817  cdlemf2  40818  trlord  40825  ltrniotacnvval  40838  cdlemg2fv2  40856  cdlemg2l  40859  cdlemg7fvbwN  40863  cdlemg4c  40868  cdlemg4  40873  cdlemg6c  40876  cdlemg8b  40884  cdlemg11b  40898  cdlemg13a  40907  cdlemg17a  40917  cdlemg17h  40924  cdlemg17  40933  cdlemg18b  40935  cdlemg19a  40939  cdlemg27a  40948  cdlemg27b  40952  cdlemg31a  40953  cdlemg31b  40954  cdlemg31d  40956  cdlemg33b0  40957  cdlemg33a  40962  cdlemg35  40969  trlcolem  40982  cdlemg42  40985  cdlemg44a  40987  cdlemg46  40991  cdlemh1  41071  cdlemh2  41072  cdlemh  41073  cdlemi1  41074  cdlemi  41076  cdlemk3  41089  cdlemk4  41090  cdlemkvcl  41098  cdlemk7  41104  cdlemk11  41105  cdlemk15  41111  cdlemk1u  41115  cdlemk7u  41126  cdlemk11u  41127  cdlemk37  41170  cdlemk39  41172  cdlemkid1  41178  cdlemkid2  41180  cdlemk48  41206  cdlemk50  41208  cdlemk51  41209  cdlemk52  41210  dia2dimlem1  41320  dia2dimlem2  41321  dia2dimlem3  41322  dia2dimlem5  41324  dia2dimlem7  41326  dia2dimlem9  41328  dia2dimlem10  41329  dia2dimlem12  41331  dia2dimlem13  41332  cdlemm10N  41374  cdlemn2  41451  cdlemn3  41453  cdlemn9  41461  cdlemn10  41462  dihjustlem  41472  dihord1  41474  dihord2pre2  41482  dihvalcqat  41495  dib2dim  41499  dih2dimb  41500  dih2dimbALTN  41501  dihord5apre  41518  dihglbcpreN  41556  dihmeetlem3N  41561  dihmeetlem6  41565  dihjatc1  41567  dihjatc2N  41568  dihjatc3  41569  dihmeetlem9N  41571  dihmeetlem10N  41572  dihmeetlem11N  41573  dihmeetlem13N  41575  dihmeetlem15N  41577  dihmeetlem16N  41578  dihmeetlem17N  41579  dihatexv2  41595  dihjatb  41672  dihjatc  41673  dihjatcclem1  41674  dihjatcclem2  41675  dihjatcclem4  41677  dihjat  41679  dihjat3  41688  dihjat5N  41693  dvh4dimat  41694