Theorem atbase 39270

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  Vcvv 3477  ∅c0 4338   class class class wbr 5147  ‘cfv 6562  Basecbs 17244  0.cp0 18480   ⋖ ccvr 39243  Atomscatm 39244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-iota 6515  df-fun 6564  df-fv 6570  df-ats 39248

This theorem is referenced by:  atssbase  39271  0ltat  39272  leatb  39273  meetat  39277  atnle0  39290  atlen0  39291  atcmp  39292  atcvreq0  39295  atncvrN  39296  atnle  39298  atnem0  39299  atlatmstc  39300  atlatle  39301  cvlexch2  39310  cvlexchb1  39311  cvlexchb2  39312  cvlatexchb1  39315  cvlatexchb2  39316  cvlatexch1  39317  cvlatexch2  39318  cvlatexch3  39319  cvlcvr1  39320  cvlcvrp  39321  cvlatcvr1  39322  cvlatcvr2  39323  cvlsupr2  39324  cvlsupr7  39329  cvlsupr8  39330  hlatjcl  39348  hlatjcom  39349  hlatjidm  39350  hlatjass  39351  hlatj32  39353  hlatj4  39355  hlatlej1  39356  atnlej1  39361  atnlej2  39362  hlrelat5N  39383  hlrelat  39384  hlrelat2  39385  exatleN  39386  cvr2N  39393  hlrelat3  39394  cvrval3  39395  cvrval5  39397  cvrexchlem  39401  cvratlem  39403  cvrat  39404  atcvr0eq  39408  lnnat  39409  cvrat2  39411  atcvrneN  39412  atcvrj1  39413  atcvrj2b  39414  atltcvr  39417  atle  39418  atlelt  39420  2atlt  39421  atexchcvrN  39422  cvrat3  39424  cvrat4  39425  cvrat42  39426  2atjm  39427  atbtwn  39428  3noncolr2  39431  4noncolr3  39435  athgt  39438  3dim0  39439  3dimlem3a  39442  3dimlem3OLDN  39444  3dimlem4a  39445  3dimlem4OLDN  39447  3dim3  39451  2dim  39452  1cvratex  39455  1cvrjat  39457  1cvrat  39458  ps-1  39459  ps-2  39460  hlatexch3N  39462  hlatexch4  39463  ps-2b  39464  3atlem1  39465  3atlem2  39466  3atlem4  39468  3atlem5  39469  3atlem6  39470  3at  39472  islln3  39492  llnnleat  39495  llnn0  39498  llnle  39500  llnexatN  39503  llncmp  39504  2llnmat  39506  2at0mat0  39507  2atm  39509  ps-2c  39510  lplni2  39519  lplnle  39522  lplnnle2at  39523  lplnn0N  39529  islpln2a  39530  2atmat  39543  lplnexllnN  39546  2llnjaN  39548  2llnm4  39552  2llnmeqat  39553  lvoli3  39559  islvol5  39561  lvoli2  39563  lvolnle3at  39564  3atnelvolN  39568  lvoln0N  39573  islvol2aN  39574  4atlem3  39578  4atlem3a  39579  4atlem3b  39580  4atlem4a  39581  4atlem4b  39582  4atlem4c  39583  4atlem4d  39584  4atlem9  39585  4atlem10a  39586  4atlem10  39588  4atlem11a  39589  4atlem11b  39590  4atlem11  39591  4atlem12a  39592  4atlem12b  39593  4atlem12  39594  4at2  39596  lplncvrlvol2  39597  2lplnja  39601  dalempeb  39621  dalemqeb  39622  dalemreb  39623  dalemseb  39624  dalemteb  39625  dalemueb  39626  dalem3  39646  dalem16  39661  dalemcceb  39671  dalem21  39676  dalem25  39680  dalem38  39692  dalem39  39693  dalem43  39697  dalem44  39698  dalem45  39699  dalem53  39707  dalem54  39708  dalem55  39709  dalem57  39711  dalem60  39714  snatpsubN  39732  linepsubN  39734  pmaple  39743  pmapat  39745  pmap1N  39749  pmapsub  39750  pmapglbx  39751  isline2  39756  linepmap  39757  isline3  39758  isline4N  39759  lneq2at  39760  lncvrelatN  39763  lncmp  39765  2lnat  39766  2atm2atN  39767  2llnma1b  39768  2llnma1  39769  2llnma3r  39770  cdlema1N  39773  cdlemblem  39775  cdlemb  39776  elpaddn0  39782  paddcom  39795  paddasslem2  39803  paddasslem5  39806  paddasslem12  39813  paddasslem13  39814  pmapjoin  39834  pmapjat1  39835  pmapjat2  39836  pmapjlln1  39837  atmod1i1  39839  atmod1i2  39841  llnmod1i2  39842  atmod2i1  39843  atmod2i2  39844  atmod3i1  39846  atmod3i2  39847  atmod4i1  39848  atmod4i2  39849  llnexchb2lem  39850  llnexchb2  39851  dalawlem2  39854  dalawlem3  39855  dalawlem5  39857  dalawlem6  39858  dalawlem7  39859  dalawlem8  39860  dalawlem11  39863  dalawlem12  39864  polval2N  39888  pol1N  39892  polatN  39913  2polatN  39914  paddatclN  39931  linepsubclN  39933  lhp2lt  39983  lhp0lt  39985  lhpexle2lem  39991  lhpexle3lem  39993  lhpjat2  40003  lhpj1  40004  lhpmcvr3  40007  lhpmcvr4N  40008  lhpmcvr5N  40009  lhpmcvr6N  40010  lhpmatb  40013  lhp2at0  40014  lhp2atnle  40015  lhp2at0nle  40017  lhprelat3N  40022  lhple  40024  lhpat4N  40026  lhpat3  40028  4atexlemtlw  40049  4atexlemc  40051  4atexlemnclw  40052  4atexlemcnd  40054  4atex2-0aOLDN  40060  lauteq  40077  ltrnid  40117  ltrnel  40121  ltrnat  40122  ltrncnvat  40123  ltrncnvel  40124  ltrncoval  40127  ltrncnv  40128  ltrn11at  40129  ltrneq2  40130  ltrneq  40131  idltrn  40132  trlval2  40145  trlcnv  40147  trljat1  40148  trljat2  40149  ltrnideq  40157  arglem1N  40172  cdlemc1  40173  cdlemc2  40174  cdlemc4  40176  cdlemc5  40177  cdlemc6  40178  cdlemd1  40180  cdlemd2  40181  cdlemd3  40182  cdlemd4  40183  cdlemd7  40186  cdleme0aa  40192  cdleme0b  40194  cdleme0c  40195  cdleme0cp  40196  cdleme0cq  40197  cdleme0e  40199  cdleme0fN  40200  cdleme1b  40208  cdleme1  40209  cdleme2  40210  cdleme3b  40211  cdleme3c  40212  cdleme3e  40214  cdleme3g  40216  cdleme3h  40217  cdleme3  40219  cdleme5  40222  cdleme7d  40228  cdleme7e  40229  cdleme7ga  40230  cdleme7  40231  cdleme8  40232  cdleme9  40235  cdleme10  40236  cdleme11c  40243  cdleme11e  40245  cdleme11fN  40246  cdleme11g  40247  cdleme11k  40250  cdleme11  40252  cdleme15b  40257  cdleme15  40260  cdleme16b  40261  cdleme17b  40269  cdleme17c  40270  cdlemednpq  40281  cdleme20zN  40283  cdleme19a  40285  cdleme20bN  40292  cdleme20d  40294  cdleme20j  40300  cdleme21c  40309  cdleme22aa  40321  cdleme22b  40323  cdleme22cN  40324  cdleme22d  40325  cdleme22e  40326  cdleme22eALTN  40327  cdleme23b  40332  cdleme23c  40333  cdleme27N  40351  cdleme28a  40352  cdleme30a  40360  cdlemefrs29pre00  40377  cdlemefrs29bpre0  40378  cdlemefrs29cpre1  40380  cdlemefrs32fva  40382  cdlemefrs32fva1  40383  cdlemefr32snb  40387  cdlemefs32snb  40397  cdleme32snb  40418  cdleme32fva  40419  cdleme32fva1  40420  cdleme32fvaw  40421  cdleme35a  40430  cdleme35fnpq  40431  cdleme35b  40432  cdleme35c  40433  cdleme35f  40436  cdleme42c  40454  cdleme42e  40461  cdleme42h  40464  cdleme42i  40465  cdleme42ke  40467  cdleme42keg  40468  cdleme42mgN  40470  cdleme17d4  40479  cdleme48fvg  40482  cdleme48bw  40484  cdlemeg46req  40511  cdleme50trn3  40535  cdlemf1  40543  cdlemf2  40544  trlord  40551  ltrniotacnvval  40564  cdlemg2fv2  40582  cdlemg2l  40585  cdlemg7fvbwN  40589  cdlemg4c  40594  cdlemg4  40599  cdlemg6c  40602  cdlemg8b  40610  cdlemg11b  40624  cdlemg13a  40633  cdlemg17a  40643  cdlemg17h  40650  cdlemg17  40659  cdlemg18b  40661  cdlemg19a  40665  cdlemg27a  40674  cdlemg27b  40678  cdlemg31a  40679  cdlemg31b  40680  cdlemg31d  40682  cdlemg33b0  40683  cdlemg33a  40688  cdlemg35  40695  trlcolem  40708  cdlemg42  40711  cdlemg44a  40713  cdlemg46  40717  cdlemh1  40797  cdlemh2  40798  cdlemh  40799  cdlemi1  40800  cdlemi  40802  cdlemk3  40815  cdlemk4  40816  cdlemkvcl  40824  cdlemk7  40830  cdlemk11  40831  cdlemk15  40837  cdlemk1u  40841  cdlemk7u  40852  cdlemk11u  40853  cdlemk37  40896  cdlemk39  40898  cdlemkid1  40904  cdlemkid2  40906  cdlemk48  40932  cdlemk50  40934  cdlemk51  40935  cdlemk52  40936  dia2dimlem1  41046  dia2dimlem2  41047  dia2dimlem3  41048  dia2dimlem5  41050  dia2dimlem7  41052  dia2dimlem9  41054  dia2dimlem10  41055  dia2dimlem12  41057  dia2dimlem13  41058  cdlemm10N  41100  cdlemn2  41177  cdlemn3  41179  cdlemn9  41187  cdlemn10  41188  dihjustlem  41198  dihord1  41200  dihord2pre2  41208  dihvalcqat  41221  dib2dim  41225  dih2dimb  41226  dih2dimbALTN  41227  dihord5apre  41244  dihglbcpreN  41282  dihmeetlem3N  41287  dihmeetlem6  41291  dihjatc1  41293  dihjatc2N  41294  dihjatc3  41295  dihmeetlem9N  41297  dihmeetlem10N  41298  dihmeetlem11N  41299  dihmeetlem13N  41301  dihmeetlem15N  41303  dihmeetlem16N  41304  dihmeetlem17N  41305  dihatexv2  41321  dihjatb  41398  dihjatc  41399  dihjatcclem1  41400  dihjatcclem2  41401  dihjatcclem4  41403  dihjat  41405  dihjat3  41414  dihjat5N  41419  dvh4dimat  41420