Theorem atbase 39735

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  Vcvv 3429  ∅c0 4273   class class class wbr 5085  ‘cfv 6498  Basecbs 17179  0.cp0 18387   ⋖ ccvr 39708  Atomscatm 39709

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  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 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6454  df-fun 6500  df-fv 6506  df-ats 39713

This theorem is referenced by:  atssbase  39736  0ltat  39737  leatb  39738  meetat  39742  atnle0  39755  atlen0  39756  atcmp  39757  atcvreq0  39760  atncvrN  39761  atnle  39763  atnem0  39764  atlatmstc  39765  atlatle  39766  cvlexch2  39775  cvlexchb1  39776  cvlexchb2  39777  cvlatexchb1  39780  cvlatexchb2  39781  cvlatexch1  39782  cvlatexch2  39783  cvlatexch3  39784  cvlcvr1  39785  cvlcvrp  39786  cvlatcvr1  39787  cvlatcvr2  39788  cvlsupr2  39789  cvlsupr7  39794  cvlsupr8  39795  hlatjcl  39813  hlatjcom  39814  hlatjidm  39815  hlatjass  39816  hlatj32  39818  hlatj4  39820  hlatlej1  39821  atnlej1  39825  atnlej2  39826  hlrelat5N  39847  hlrelat  39848  hlrelat2  39849  exatleN  39850  cvr2N  39857  hlrelat3  39858  cvrval3  39859  cvrval5  39861  cvrexchlem  39865  cvratlem  39867  cvrat  39868  atcvr0eq  39872  lnnat  39873  cvrat2  39875  atcvrneN  39876  atcvrj1  39877  atcvrj2b  39878  atltcvr  39881  atle  39882  atlelt  39884  2atlt  39885  atexchcvrN  39886  cvrat3  39888  cvrat4  39889  cvrat42  39890  2atjm  39891  atbtwn  39892  3noncolr2  39895  4noncolr3  39899  athgt  39902  3dim0  39903  3dimlem3a  39906  3dimlem3OLDN  39908  3dimlem4a  39909  3dimlem4OLDN  39911  3dim3  39915  2dim  39916  1cvratex  39919  1cvrjat  39921  1cvrat  39922  ps-1  39923  ps-2  39924  hlatexch3N  39926  hlatexch4  39927  ps-2b  39928  3atlem1  39929  3atlem2  39930  3atlem4  39932  3atlem5  39933  3atlem6  39934  3at  39936  islln3  39956  llnnleat  39959  llnn0  39962  llnle  39964  llnexatN  39967  llncmp  39968  2llnmat  39970  2at0mat0  39971  2atm  39973  ps-2c  39974  lplni2  39983  lplnle  39986  lplnnle2at  39987  lplnn0N  39993  islpln2a  39994  2atmat  40007  lplnexllnN  40010  2llnjaN  40012  2llnm4  40016  2llnmeqat  40017  lvoli3  40023  islvol5  40025  lvoli2  40027  lvolnle3at  40028  3atnelvolN  40032  lvoln0N  40037  islvol2aN  40038  4atlem3  40042  4atlem3a  40043  4atlem3b  40044  4atlem4a  40045  4atlem4b  40046  4atlem4c  40047  4atlem4d  40048  4atlem9  40049  4atlem10a  40050  4atlem10  40052  4atlem11a  40053  4atlem11b  40054  4atlem11  40055  4atlem12a  40056  4atlem12b  40057  4atlem12  40058  4at2  40060  lplncvrlvol2  40061  2lplnja  40065  dalempeb  40085  dalemqeb  40086  dalemreb  40087  dalemseb  40088  dalemteb  40089  dalemueb  40090  dalem3  40110  dalem16  40125  dalemcceb  40135  dalem21  40140  dalem25  40144  dalem38  40156  dalem39  40157  dalem43  40161  dalem44  40162  dalem45  40163  dalem53  40171  dalem54  40172  dalem55  40173  dalem57  40175  dalem60  40178  snatpsubN  40196  linepsubN  40198  pmaple  40207  pmapat  40209  pmap1N  40213  pmapsub  40214  pmapglbx  40215  isline2  40220  linepmap  40221  isline3  40222  isline4N  40223  lneq2at  40224  lncvrelatN  40227  lncmp  40229  2lnat  40230  2atm2atN  40231  2llnma1b  40232  2llnma1  40233  2llnma3r  40234  cdlema1N  40237  cdlemblem  40239  cdlemb  40240  elpaddn0  40246  paddcom  40259  paddasslem2  40267  paddasslem5  40270  paddasslem12  40277  paddasslem13  40278  pmapjoin  40298  pmapjat1  40299  pmapjat2  40300  pmapjlln1  40301  atmod1i1  40303  atmod1i2  40305  llnmod1i2  40306  atmod2i1  40307  atmod2i2  40308  atmod3i1  40310  atmod3i2  40311  atmod4i1  40312  atmod4i2  40313  llnexchb2lem  40314  llnexchb2  40315  dalawlem2  40318  dalawlem3  40319  dalawlem5  40321  dalawlem6  40322  dalawlem7  40323  dalawlem8  40324  dalawlem11  40327  dalawlem12  40328  polval2N  40352  pol1N  40356  polatN  40377  2polatN  40378  paddatclN  40395  linepsubclN  40397  lhp2lt  40447  lhp0lt  40449  lhpexle2lem  40455  lhpexle3lem  40457  lhpjat2  40467  lhpj1  40468  lhpmcvr3  40471  lhpmcvr4N  40472  lhpmcvr5N  40473  lhpmcvr6N  40474  lhpmatb  40477  lhp2at0  40478  lhp2atnle  40479  lhp2at0nle  40481  lhprelat3N  40486  lhple  40488  lhpat4N  40490  lhpat3  40492  4atexlemtlw  40513  4atexlemc  40515  4atexlemnclw  40516  4atexlemcnd  40518  4atex2-0aOLDN  40524  lauteq  40541  ltrnid  40581  ltrnel  40585  ltrnat  40586  ltrncnvat  40587  ltrncnvel  40588  ltrncoval  40591  ltrncnv  40592  ltrn11at  40593  ltrneq2  40594  ltrneq  40595  idltrn  40596  trlval2  40609  trlcnv  40611  trljat1  40612  trljat2  40613  ltrnideq  40621  arglem1N  40636  cdlemc1  40637  cdlemc2  40638  cdlemc4  40640  cdlemc5  40641  cdlemc6  40642  cdlemd1  40644  cdlemd2  40645  cdlemd3  40646  cdlemd4  40647  cdlemd7  40650  cdleme0aa  40656  cdleme0b  40658  cdleme0c  40659  cdleme0cp  40660  cdleme0cq  40661  cdleme0e  40663  cdleme0fN  40664  cdleme1b  40672  cdleme1  40673  cdleme2  40674  cdleme3b  40675  cdleme3c  40676  cdleme3e  40678  cdleme3g  40680  cdleme3h  40681  cdleme3  40683  cdleme5  40686  cdleme7d  40692  cdleme7e  40693  cdleme7ga  40694  cdleme7  40695  cdleme8  40696  cdleme9  40699  cdleme10  40700  cdleme11c  40707  cdleme11e  40709  cdleme11fN  40710  cdleme11g  40711  cdleme11k  40714  cdleme11  40716  cdleme15b  40721  cdleme15  40724  cdleme16b  40725  cdleme17b  40733  cdleme17c  40734  cdlemednpq  40745  cdleme20zN  40747  cdleme19a  40749  cdleme20bN  40756  cdleme20d  40758  cdleme20j  40764  cdleme21c  40773  cdleme22aa  40785  cdleme22b  40787  cdleme22cN  40788  cdleme22d  40789  cdleme22e  40790  cdleme22eALTN  40791  cdleme23b  40796  cdleme23c  40797  cdleme27N  40815  cdleme28a  40816  cdleme30a  40824  cdlemefrs29pre00  40841  cdlemefrs29bpre0  40842  cdlemefrs29cpre1  40844  cdlemefrs32fva  40846  cdlemefrs32fva1  40847  cdlemefr32snb  40851  cdlemefs32snb  40861  cdleme32snb  40882  cdleme32fva  40883  cdleme32fva1  40884  cdleme32fvaw  40885  cdleme35a  40894  cdleme35fnpq  40895  cdleme35b  40896  cdleme35c  40897  cdleme35f  40900  cdleme42c  40918  cdleme42e  40925  cdleme42h  40928  cdleme42i  40929  cdleme42ke  40931  cdleme42keg  40932  cdleme42mgN  40934  cdleme17d4  40943  cdleme48fvg  40946  cdleme48bw  40948  cdlemeg46req  40975  cdleme50trn3  40999  cdlemf1  41007  cdlemf2  41008  trlord  41015  ltrniotacnvval  41028  cdlemg2fv2  41046  cdlemg2l  41049  cdlemg7fvbwN  41053  cdlemg4c  41058  cdlemg4  41063  cdlemg6c  41066  cdlemg8b  41074  cdlemg11b  41088  cdlemg13a  41097  cdlemg17a  41107  cdlemg17h  41114  cdlemg17  41123  cdlemg18b  41125  cdlemg19a  41129  cdlemg27a  41138  cdlemg27b  41142  cdlemg31a  41143  cdlemg31b  41144  cdlemg31d  41146  cdlemg33b0  41147  cdlemg33a  41152  cdlemg35  41159  trlcolem  41172  cdlemg42  41175  cdlemg44a  41177  cdlemg46  41181  cdlemh1  41261  cdlemh2  41262  cdlemh  41263  cdlemi1  41264  cdlemi  41266  cdlemk3  41279  cdlemk4  41280  cdlemkvcl  41288  cdlemk7  41294  cdlemk11  41295  cdlemk15  41301  cdlemk1u  41305  cdlemk7u  41316  cdlemk11u  41317  cdlemk37  41360  cdlemk39  41362  cdlemkid1  41368  cdlemkid2  41370  cdlemk48  41396  cdlemk50  41398  cdlemk51  41399  cdlemk52  41400  dia2dimlem1  41510  dia2dimlem2  41511  dia2dimlem3  41512  dia2dimlem5  41514  dia2dimlem7  41516  dia2dimlem9  41518  dia2dimlem10  41519  dia2dimlem12  41521  dia2dimlem13  41522  cdlemm10N  41564  cdlemn2  41641  cdlemn3  41643  cdlemn9  41651  cdlemn10  41652  dihjustlem  41662  dihord1  41664  dihord2pre2  41672  dihvalcqat  41685  dib2dim  41689  dih2dimb  41690  dih2dimbALTN  41691  dihord5apre  41708  dihglbcpreN  41746  dihmeetlem3N  41751  dihmeetlem6  41755  dihjatc1  41757  dihjatc2N  41758  dihjatc3  41759  dihmeetlem9N  41761  dihmeetlem10N  41762  dihmeetlem11N  41763  dihmeetlem13N  41765  dihmeetlem15N  41767  dihmeetlem16N  41768  dihmeetlem17N  41769  dihatexv2  41785  dihjatb  41862  dihjatc  41863  dihjatcclem1  41864  dihjatcclem2  41865  dihjatcclem4  41867  dihjat  41869  dihjat3  41878  dihjat5N  41883  dvh4dimat  41884