Theorem atbase 37824

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 31349 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 4298	. . . 4 ⊢ (𝑃 ∈ 𝐴 → ¬ 𝐴 = ∅)
2		atombase.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
3	2	eqeq1i 2736	. . . 4 ⊢ (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
4	1, 3	sylnib 327	. . 3 ⊢ (𝑃 ∈ 𝐴 → ¬ (Atoms‘𝐾) = ∅)
5		fvprc 6839	. . 3 ⊢ (¬ 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
6	4, 5	nsyl2 141	. 2 ⊢ (𝑃 ∈ 𝐴 → 𝐾 ∈ V)
7		atombase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2731	. . . 4 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		eqid 2731	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	isat 37821	. . 3 ⊢ (𝐾 ∈ V → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
11	10	simprbda 499	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐵)
12	6, 11	mpancom 686	1 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  Vcvv 3446  ∅c0 4287   class class class wbr 5110  ‘cfv 6501  Basecbs 17094  0.cp0 18326   ⋖ ccvr 37797  Atomscatm 37798

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6453  df-fun 6503  df-fv 6509  df-ats 37802

This theorem is referenced by:  atssbase  37825  0ltat  37826  leatb  37827  meetat  37831  atnle0  37844  atlen0  37845  atcmp  37846  atcvreq0  37849  atncvrN  37850  atnle  37852  atnem0  37853  atlatmstc  37854  atlatle  37855  cvlexch2  37864  cvlexchb1  37865  cvlexchb2  37866  cvlatexchb1  37869  cvlatexchb2  37870  cvlatexch1  37871  cvlatexch2  37872  cvlatexch3  37873  cvlcvr1  37874  cvlcvrp  37875  cvlatcvr1  37876  cvlatcvr2  37877  cvlsupr2  37878  cvlsupr7  37883  cvlsupr8  37884  hlatjcl  37902  hlatjcom  37903  hlatjidm  37904  hlatjass  37905  hlatj32  37907  hlatj4  37909  hlatlej1  37910  atnlej1  37915  atnlej2  37916  hlrelat5N  37937  hlrelat  37938  hlrelat2  37939  exatleN  37940  cvr2N  37947  hlrelat3  37948  cvrval3  37949  cvrval5  37951  cvrexchlem  37955  cvratlem  37957  cvrat  37958  atcvr0eq  37962  lnnat  37963  cvrat2  37965  atcvrneN  37966  atcvrj1  37967  atcvrj2b  37968  atltcvr  37971  atle  37972  atlelt  37974  2atlt  37975  atexchcvrN  37976  cvrat3  37978  cvrat4  37979  cvrat42  37980  2atjm  37981  atbtwn  37982  3noncolr2  37985  4noncolr3  37989  athgt  37992  3dim0  37993  3dimlem3a  37996  3dimlem3OLDN  37998  3dimlem4a  37999  3dimlem4OLDN  38001  3dim3  38005  2dim  38006  1cvratex  38009  1cvrjat  38011  1cvrat  38012  ps-1  38013  ps-2  38014  hlatexch3N  38016  hlatexch4  38017  ps-2b  38018  3atlem1  38019  3atlem2  38020  3atlem4  38022  3atlem5  38023  3atlem6  38024  3at  38026  islln3  38046  llnnleat  38049  llnn0  38052  llnle  38054  llnexatN  38057  llncmp  38058  2llnmat  38060  2at0mat0  38061  2atm  38063  ps-2c  38064  lplni2  38073  lplnle  38076  lplnnle2at  38077  lplnn0N  38083  islpln2a  38084  2atmat  38097  lplnexllnN  38100  2llnjaN  38102  2llnm4  38106  2llnmeqat  38107  lvoli3  38113  islvol5  38115  lvoli2  38117  lvolnle3at  38118  3atnelvolN  38122  lvoln0N  38127  islvol2aN  38128  4atlem3  38132  4atlem3a  38133  4atlem3b  38134  4atlem4a  38135  4atlem4b  38136  4atlem4c  38137  4atlem4d  38138  4atlem9  38139  4atlem10a  38140  4atlem10  38142  4atlem11a  38143  4atlem11b  38144  4atlem11  38145  4atlem12a  38146  4atlem12b  38147  4atlem12  38148  4at2  38150  lplncvrlvol2  38151  2lplnja  38155  dalempeb  38175  dalemqeb  38176  dalemreb  38177  dalemseb  38178  dalemteb  38179  dalemueb  38180  dalem3  38200  dalem16  38215  dalemcceb  38225  dalem21  38230  dalem25  38234  dalem38  38246  dalem39  38247  dalem43  38251  dalem44  38252  dalem45  38253  dalem53  38261  dalem54  38262  dalem55  38263  dalem57  38265  dalem60  38268  snatpsubN  38286  linepsubN  38288  pmaple  38297  pmapat  38299  pmap1N  38303  pmapsub  38304  pmapglbx  38305  isline2  38310  linepmap  38311  isline3  38312  isline4N  38313  lneq2at  38314  lncvrelatN  38317  lncmp  38319  2lnat  38320  2atm2atN  38321  2llnma1b  38322  2llnma1  38323  2llnma3r  38324  cdlema1N  38327  cdlemblem  38329  cdlemb  38330  elpaddn0  38336  paddcom  38349  paddasslem2  38357  paddasslem5  38360  paddasslem12  38367  paddasslem13  38368  pmapjoin  38388  pmapjat1  38389  pmapjat2  38390  pmapjlln1  38391  atmod1i1  38393  atmod1i2  38395  llnmod1i2  38396  atmod2i1  38397  atmod2i2  38398  atmod3i1  38400  atmod3i2  38401  atmod4i1  38402  atmod4i2  38403  llnexchb2lem  38404  llnexchb2  38405  dalawlem2  38408  dalawlem3  38409  dalawlem5  38411  dalawlem6  38412  dalawlem7  38413  dalawlem8  38414  dalawlem11  38417  dalawlem12  38418  polval2N  38442  pol1N  38446  polatN  38467  2polatN  38468  paddatclN  38485  linepsubclN  38487  lhp2lt  38537  lhp0lt  38539  lhpexle2lem  38545  lhpexle3lem  38547  lhpjat2  38557  lhpj1  38558  lhpmcvr3  38561  lhpmcvr4N  38562  lhpmcvr5N  38563  lhpmcvr6N  38564  lhpmatb  38567  lhp2at0  38568  lhp2atnle  38569  lhp2at0nle  38571  lhprelat3N  38576  lhple  38578  lhpat4N  38580  lhpat3  38582  4atexlemtlw  38603  4atexlemc  38605  4atexlemnclw  38606  4atexlemcnd  38608  4atex2-0aOLDN  38614  lauteq  38631  ltrnid  38671  ltrnel  38675  ltrnat  38676  ltrncnvat  38677  ltrncnvel  38678  ltrncoval  38681  ltrncnv  38682  ltrn11at  38683  ltrneq2  38684  ltrneq  38685  idltrn  38686  trlval2  38699  trlcnv  38701  trljat1  38702  trljat2  38703  ltrnideq  38711  arglem1N  38726  cdlemc1  38727  cdlemc2  38728  cdlemc4  38730  cdlemc5  38731  cdlemc6  38732  cdlemd1  38734  cdlemd2  38735  cdlemd3  38736  cdlemd4  38737  cdlemd7  38740  cdleme0aa  38746  cdleme0b  38748  cdleme0c  38749  cdleme0cp  38750  cdleme0cq  38751  cdleme0e  38753  cdleme0fN  38754  cdleme1b  38762  cdleme1  38763  cdleme2  38764  cdleme3b  38765  cdleme3c  38766  cdleme3e  38768  cdleme3g  38770  cdleme3h  38771  cdleme3  38773  cdleme5  38776  cdleme7d  38782  cdleme7e  38783  cdleme7ga  38784  cdleme7  38785  cdleme8  38786  cdleme9  38789  cdleme10  38790  cdleme11c  38797  cdleme11e  38799  cdleme11fN  38800  cdleme11g  38801  cdleme11k  38804  cdleme11  38806  cdleme15b  38811  cdleme15  38814  cdleme16b  38815  cdleme17b  38823  cdleme17c  38824  cdlemednpq  38835  cdleme20zN  38837  cdleme19a  38839  cdleme20bN  38846  cdleme20d  38848  cdleme20j  38854  cdleme21c  38863  cdleme22aa  38875  cdleme22b  38877  cdleme22cN  38878  cdleme22d  38879  cdleme22e  38880  cdleme22eALTN  38881  cdleme23b  38886  cdleme23c  38887  cdleme27N  38905  cdleme28a  38906  cdleme30a  38914  cdlemefrs29pre00  38931  cdlemefrs29bpre0  38932  cdlemefrs29cpre1  38934  cdlemefrs32fva  38936  cdlemefrs32fva1  38937  cdlemefr32snb  38941  cdlemefs32snb  38951  cdleme32snb  38972  cdleme32fva  38973  cdleme32fva1  38974  cdleme32fvaw  38975  cdleme35a  38984  cdleme35fnpq  38985  cdleme35b  38986  cdleme35c  38987  cdleme35f  38990  cdleme42c  39008  cdleme42e  39015  cdleme42h  39018  cdleme42i  39019  cdleme42ke  39021  cdleme42keg  39022  cdleme42mgN  39024  cdleme17d4  39033  cdleme48fvg  39036  cdleme48bw  39038  cdlemeg46req  39065  cdleme50trn3  39089  cdlemf1  39097  cdlemf2  39098  trlord  39105  ltrniotacnvval  39118  cdlemg2fv2  39136  cdlemg2l  39139  cdlemg7fvbwN  39143  cdlemg4c  39148  cdlemg4  39153  cdlemg6c  39156  cdlemg8b  39164  cdlemg11b  39178  cdlemg13a  39187  cdlemg17a  39197  cdlemg17h  39204  cdlemg17  39213  cdlemg18b  39215  cdlemg19a  39219  cdlemg27a  39228  cdlemg27b  39232  cdlemg31a  39233  cdlemg31b  39234  cdlemg31d  39236  cdlemg33b0  39237  cdlemg33a  39242  cdlemg35  39249  trlcolem  39262  cdlemg42  39265  cdlemg44a  39267  cdlemg46  39271  cdlemh1  39351  cdlemh2  39352  cdlemh  39353  cdlemi1  39354  cdlemi  39356  cdlemk3  39369  cdlemk4  39370  cdlemkvcl  39378  cdlemk7  39384  cdlemk11  39385  cdlemk15  39391  cdlemk1u  39395  cdlemk7u  39406  cdlemk11u  39407  cdlemk37  39450  cdlemk39  39452  cdlemkid1  39458  cdlemkid2  39460  cdlemk48  39486  cdlemk50  39488  cdlemk51  39489  cdlemk52  39490  dia2dimlem1  39600  dia2dimlem2  39601  dia2dimlem3  39602  dia2dimlem5  39604  dia2dimlem7  39606  dia2dimlem9  39608  dia2dimlem10  39609  dia2dimlem12  39611  dia2dimlem13  39612  cdlemm10N  39654  cdlemn2  39731  cdlemn3  39733  cdlemn9  39741  cdlemn10  39742  dihjustlem  39752  dihord1  39754  dihord2pre2  39762  dihvalcqat  39775  dib2dim  39779  dih2dimb  39780  dih2dimbALTN  39781  dihord5apre  39798  dihglbcpreN  39836  dihmeetlem3N  39841  dihmeetlem6  39845  dihjatc1  39847  dihjatc2N  39848  dihjatc3  39849  dihmeetlem9N  39851  dihmeetlem10N  39852  dihmeetlem11N  39853  dihmeetlem13N  39855  dihmeetlem15N  39857  dihmeetlem16N  39858  dihmeetlem17N  39859  dihatexv2  39875  dihjatb  39952  dihjatc  39953  dihjatcclem1  39954  dihjatcclem2  39955  dihjatcclem4  39957  dihjat  39959  dihjat3  39968  dihjat5N  39973  dvh4dimat  39974