Theorem atbase 39267

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3438  ∅c0 4286   class class class wbr 5095  ‘cfv 6486  Basecbs 17138  0.cp0 18345   ⋖ ccvr 39240  Atomscatm 39241

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 5238  ax-nul 5248  ax-pr 5374

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fv 6494  df-ats 39245

This theorem is referenced by:  atssbase  39268  0ltat  39269  leatb  39270  meetat  39274  atnle0  39287  atlen0  39288  atcmp  39289  atcvreq0  39292  atncvrN  39293  atnle  39295  atnem0  39296  atlatmstc  39297  atlatle  39298  cvlexch2  39307  cvlexchb1  39308  cvlexchb2  39309  cvlatexchb1  39312  cvlatexchb2  39313  cvlatexch1  39314  cvlatexch2  39315  cvlatexch3  39316  cvlcvr1  39317  cvlcvrp  39318  cvlatcvr1  39319  cvlatcvr2  39320  cvlsupr2  39321  cvlsupr7  39326  cvlsupr8  39327  hlatjcl  39345  hlatjcom  39346  hlatjidm  39347  hlatjass  39348  hlatj32  39350  hlatj4  39352  hlatlej1  39353  atnlej1  39358  atnlej2  39359  hlrelat5N  39380  hlrelat  39381  hlrelat2  39382  exatleN  39383  cvr2N  39390  hlrelat3  39391  cvrval3  39392  cvrval5  39394  cvrexchlem  39398  cvratlem  39400  cvrat  39401  atcvr0eq  39405  lnnat  39406  cvrat2  39408  atcvrneN  39409  atcvrj1  39410  atcvrj2b  39411  atltcvr  39414  atle  39415  atlelt  39417  2atlt  39418  atexchcvrN  39419  cvrat3  39421  cvrat4  39422  cvrat42  39423  2atjm  39424  atbtwn  39425  3noncolr2  39428  4noncolr3  39432  athgt  39435  3dim0  39436  3dimlem3a  39439  3dimlem3OLDN  39441  3dimlem4a  39442  3dimlem4OLDN  39444  3dim3  39448  2dim  39449  1cvratex  39452  1cvrjat  39454  1cvrat  39455  ps-1  39456  ps-2  39457  hlatexch3N  39459  hlatexch4  39460  ps-2b  39461  3atlem1  39462  3atlem2  39463  3atlem4  39465  3atlem5  39466  3atlem6  39467  3at  39469  islln3  39489  llnnleat  39492  llnn0  39495  llnle  39497  llnexatN  39500  llncmp  39501  2llnmat  39503  2at0mat0  39504  2atm  39506  ps-2c  39507  lplni2  39516  lplnle  39519  lplnnle2at  39520  lplnn0N  39526  islpln2a  39527  2atmat  39540  lplnexllnN  39543  2llnjaN  39545  2llnm4  39549  2llnmeqat  39550  lvoli3  39556  islvol5  39558  lvoli2  39560  lvolnle3at  39561  3atnelvolN  39565  lvoln0N  39570  islvol2aN  39571  4atlem3  39575  4atlem3a  39576  4atlem3b  39577  4atlem4a  39578  4atlem4b  39579  4atlem4c  39580  4atlem4d  39581  4atlem9  39582  4atlem10a  39583  4atlem10  39585  4atlem11a  39586  4atlem11b  39587  4atlem11  39588  4atlem12a  39589  4atlem12b  39590  4atlem12  39591  4at2  39593  lplncvrlvol2  39594  2lplnja  39598  dalempeb  39618  dalemqeb  39619  dalemreb  39620  dalemseb  39621  dalemteb  39622  dalemueb  39623  dalem3  39643  dalem16  39658  dalemcceb  39668  dalem21  39673  dalem25  39677  dalem38  39689  dalem39  39690  dalem43  39694  dalem44  39695  dalem45  39696  dalem53  39704  dalem54  39705  dalem55  39706  dalem57  39708  dalem60  39711  snatpsubN  39729  linepsubN  39731  pmaple  39740  pmapat  39742  pmap1N  39746  pmapsub  39747  pmapglbx  39748  isline2  39753  linepmap  39754  isline3  39755  isline4N  39756  lneq2at  39757  lncvrelatN  39760  lncmp  39762  2lnat  39763  2atm2atN  39764  2llnma1b  39765  2llnma1  39766  2llnma3r  39767  cdlema1N  39770  cdlemblem  39772  cdlemb  39773  elpaddn0  39779  paddcom  39792  paddasslem2  39800  paddasslem5  39803  paddasslem12  39810  paddasslem13  39811  pmapjoin  39831  pmapjat1  39832  pmapjat2  39833  pmapjlln1  39834  atmod1i1  39836  atmod1i2  39838  llnmod1i2  39839  atmod2i1  39840  atmod2i2  39841  atmod3i1  39843  atmod3i2  39844  atmod4i1  39845  atmod4i2  39846  llnexchb2lem  39847  llnexchb2  39848  dalawlem2  39851  dalawlem3  39852  dalawlem5  39854  dalawlem6  39855  dalawlem7  39856  dalawlem8  39857  dalawlem11  39860  dalawlem12  39861  polval2N  39885  pol1N  39889  polatN  39910  2polatN  39911  paddatclN  39928  linepsubclN  39930  lhp2lt  39980  lhp0lt  39982  lhpexle2lem  39988  lhpexle3lem  39990  lhpjat2  40000  lhpj1  40001  lhpmcvr3  40004  lhpmcvr4N  40005  lhpmcvr5N  40006  lhpmcvr6N  40007  lhpmatb  40010  lhp2at0  40011  lhp2atnle  40012  lhp2at0nle  40014  lhprelat3N  40019  lhple  40021  lhpat4N  40023  lhpat3  40025  4atexlemtlw  40046  4atexlemc  40048  4atexlemnclw  40049  4atexlemcnd  40051  4atex2-0aOLDN  40057  lauteq  40074  ltrnid  40114  ltrnel  40118  ltrnat  40119  ltrncnvat  40120  ltrncnvel  40121  ltrncoval  40124  ltrncnv  40125  ltrn11at  40126  ltrneq2  40127  ltrneq  40128  idltrn  40129  trlval2  40142  trlcnv  40144  trljat1  40145  trljat2  40146  ltrnideq  40154  arglem1N  40169  cdlemc1  40170  cdlemc2  40171  cdlemc4  40173  cdlemc5  40174  cdlemc6  40175  cdlemd1  40177  cdlemd2  40178  cdlemd3  40179  cdlemd4  40180  cdlemd7  40183  cdleme0aa  40189  cdleme0b  40191  cdleme0c  40192  cdleme0cp  40193  cdleme0cq  40194  cdleme0e  40196  cdleme0fN  40197  cdleme1b  40205  cdleme1  40206  cdleme2  40207  cdleme3b  40208  cdleme3c  40209  cdleme3e  40211  cdleme3g  40213  cdleme3h  40214  cdleme3  40216  cdleme5  40219  cdleme7d  40225  cdleme7e  40226  cdleme7ga  40227  cdleme7  40228  cdleme8  40229  cdleme9  40232  cdleme10  40233  cdleme11c  40240  cdleme11e  40242  cdleme11fN  40243  cdleme11g  40244  cdleme11k  40247  cdleme11  40249  cdleme15b  40254  cdleme15  40257  cdleme16b  40258  cdleme17b  40266  cdleme17c  40267  cdlemednpq  40278  cdleme20zN  40280  cdleme19a  40282  cdleme20bN  40289  cdleme20d  40291  cdleme20j  40297  cdleme21c  40306  cdleme22aa  40318  cdleme22b  40320  cdleme22cN  40321  cdleme22d  40322  cdleme22e  40323  cdleme22eALTN  40324  cdleme23b  40329  cdleme23c  40330  cdleme27N  40348  cdleme28a  40349  cdleme30a  40357  cdlemefrs29pre00  40374  cdlemefrs29bpre0  40375  cdlemefrs29cpre1  40377  cdlemefrs32fva  40379  cdlemefrs32fva1  40380  cdlemefr32snb  40384  cdlemefs32snb  40394  cdleme32snb  40415  cdleme32fva  40416  cdleme32fva1  40417  cdleme32fvaw  40418  cdleme35a  40427  cdleme35fnpq  40428  cdleme35b  40429  cdleme35c  40430  cdleme35f  40433  cdleme42c  40451  cdleme42e  40458  cdleme42h  40461  cdleme42i  40462  cdleme42ke  40464  cdleme42keg  40465  cdleme42mgN  40467  cdleme17d4  40476  cdleme48fvg  40479  cdleme48bw  40481  cdlemeg46req  40508  cdleme50trn3  40532  cdlemf1  40540  cdlemf2  40541  trlord  40548  ltrniotacnvval  40561  cdlemg2fv2  40579  cdlemg2l  40582  cdlemg7fvbwN  40586  cdlemg4c  40591  cdlemg4  40596  cdlemg6c  40599  cdlemg8b  40607  cdlemg11b  40621  cdlemg13a  40630  cdlemg17a  40640  cdlemg17h  40647  cdlemg17  40656  cdlemg18b  40658  cdlemg19a  40662  cdlemg27a  40671  cdlemg27b  40675  cdlemg31a  40676  cdlemg31b  40677  cdlemg31d  40679  cdlemg33b0  40680  cdlemg33a  40685  cdlemg35  40692  trlcolem  40705  cdlemg42  40708  cdlemg44a  40710  cdlemg46  40714  cdlemh1  40794  cdlemh2  40795  cdlemh  40796  cdlemi1  40797  cdlemi  40799  cdlemk3  40812  cdlemk4  40813  cdlemkvcl  40821  cdlemk7  40827  cdlemk11  40828  cdlemk15  40834  cdlemk1u  40838  cdlemk7u  40849  cdlemk11u  40850  cdlemk37  40893  cdlemk39  40895  cdlemkid1  40901  cdlemkid2  40903  cdlemk48  40929  cdlemk50  40931  cdlemk51  40932  cdlemk52  40933  dia2dimlem1  41043  dia2dimlem2  41044  dia2dimlem3  41045  dia2dimlem5  41047  dia2dimlem7  41049  dia2dimlem9  41051  dia2dimlem10  41052  dia2dimlem12  41054  dia2dimlem13  41055  cdlemm10N  41097  cdlemn2  41174  cdlemn3  41176  cdlemn9  41184  cdlemn10  41185  dihjustlem  41195  dihord1  41197  dihord2pre2  41205  dihvalcqat  41218  dib2dim  41222  dih2dimb  41223  dih2dimbALTN  41224  dihord5apre  41241  dihglbcpreN  41279  dihmeetlem3N  41284  dihmeetlem6  41288  dihjatc1  41290  dihjatc2N  41291  dihjatc3  41292  dihmeetlem9N  41294  dihmeetlem10N  41295  dihmeetlem11N  41296  dihmeetlem13N  41298  dihmeetlem15N  41300  dihmeetlem16N  41301  dihmeetlem17N  41302  dihatexv2  41318  dihjatb  41395  dihjatc  41396  dihjatcclem1  41397  dihjatcclem2  41398  dihjatcclem4  41400  dihjat  41402  dihjat3  41411  dihjat5N  41416  dvh4dimat  41417