Theorem atbase 39877

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 32493 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 2766	. . . 4 ⊢ (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
4	1, 3	sylnib 330	. . 3 ⊢ (𝑃 ∈ 𝐴 → ¬ (Atoms‘𝐾) = ∅)
5		fvprc 6855	. . 3 ⊢ (¬ 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
6	4, 5	nsyl2 141	. 2 ⊢ (𝑃 ∈ 𝐴 → 𝐾 ∈ V)
7		atombase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2761	. . . 4 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		eqid 2761	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	isat 39874	. . 3 ⊢ (𝐾 ∈ V → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
11	10	simprbda 502	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐵)
12	6, 11	mpancom 698	1 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  Vcvv 3453  ∅c0 4285   class class class wbr 5099  ‘cfv 6517  Basecbs 17228  0.cp0 18436   ⋖ ccvr 39850  Atomscatm 39851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-iota 6473  df-fun 6519  df-fv 6525  df-ats 39855

This theorem is referenced by:  atssbase  39878  0ltat  39879  leatb  39880  meetat  39884  atnle0  39897  atlen0  39898  atcmp  39899  atcvreq0  39902  atncvrN  39903  atnle  39905  atnem0  39906  atlatmstc  39907  atlatle  39908  cvlexch2  39917  cvlexchb1  39918  cvlexchb2  39919  cvlatexchb1  39922  cvlatexchb2  39923  cvlatexch1  39924  cvlatexch2  39925  cvlatexch3  39926  cvlcvr1  39927  cvlcvrp  39928  cvlatcvr1  39929  cvlatcvr2  39930  cvlsupr2  39931  cvlsupr7  39936  cvlsupr8  39937  hlatjcl  39955  hlatjcom  39956  hlatjidm  39957  hlatjass  39958  hlatj32  39960  hlatj4  39962  hlatlej1  39963  atnlej1  39967  atnlej2  39968  hlrelat5N  39989  hlrelat  39990  hlrelat2  39991  exatleN  39992  cvr2N  39999  hlrelat3  40000  cvrval3  40001  cvrval5  40003  cvrexchlem  40007  cvratlem  40009  cvrat  40010  atcvr0eq  40014  lnnat  40015  cvrat2  40017  atcvrneN  40018  atcvrj1  40019  atcvrj2b  40020  atltcvr  40023  atle  40024  atlelt  40026  2atlt  40027  atexchcvrN  40028  cvrat3  40030  cvrat4  40031  cvrat42  40032  2atjm  40033  atbtwn  40034  3noncolr2  40037  4noncolr3  40041  athgt  40044  3dim0  40045  3dimlem3a  40048  3dimlem3OLDN  40050  3dimlem4a  40051  3dimlem4OLDN  40053  3dim3  40057  2dim  40058  1cvratex  40061  1cvrjat  40063  1cvrat  40064  ps-1  40065  ps-2  40066  hlatexch3N  40068  hlatexch4  40069  ps-2b  40070  3atlem1  40071  3atlem2  40072  3atlem4  40074  3atlem5  40075  3atlem6  40076  3at  40078  islln3  40098  llnnleat  40101  llnn0  40104  llnle  40106  llnexatN  40109  llncmp  40110  2llnmat  40112  2at0mat0  40113  2atm  40115  ps-2c  40116  lplni2  40125  lplnle  40128  lplnnle2at  40129  lplnn0N  40135  islpln2a  40136  2atmat  40149  lplnexllnN  40152  2llnjaN  40154  2llnm4  40158  2llnmeqat  40159  lvoli3  40165  islvol5  40167  lvoli2  40169  lvolnle3at  40170  3atnelvolN  40174  lvoln0N  40179  islvol2aN  40180  4atlem3  40184  4atlem3a  40185  4atlem3b  40186  4atlem4a  40187  4atlem4b  40188  4atlem4c  40189  4atlem4d  40190  4atlem9  40191  4atlem10a  40192  4atlem10  40194  4atlem11a  40195  4atlem11b  40196  4atlem11  40197  4atlem12a  40198  4atlem12b  40199  4atlem12  40200  4at2  40202  lplncvrlvol2  40203  2lplnja  40207  dalempeb  40227  dalemqeb  40228  dalemreb  40229  dalemseb  40230  dalemteb  40231  dalemueb  40232  dalem3  40252  dalem16  40267  dalemcceb  40277  dalem21  40282  dalem25  40286  dalem38  40298  dalem39  40299  dalem43  40303  dalem44  40304  dalem45  40305  dalem53  40313  dalem54  40314  dalem55  40315  dalem57  40317  dalem60  40320  snatpsubN  40338  linepsubN  40340  pmaple  40349  pmapat  40351  pmap1N  40355  pmapsub  40356  pmapglbx  40357  isline2  40362  linepmap  40363  isline3  40364  isline4N  40365  lneq2at  40366  lncvrelatN  40369  lncmp  40371  2lnat  40372  2atm2atN  40373  2llnma1b  40374  2llnma1  40375  2llnma3r  40376  cdlema1N  40379  cdlemblem  40381  cdlemb  40382  elpaddn0  40388  paddcom  40401  paddasslem2  40409  paddasslem5  40412  paddasslem12  40419  paddasslem13  40420  pmapjoin  40440  pmapjat1  40441  pmapjat2  40442  pmapjlln1  40443  atmod1i1  40445  atmod1i2  40447  llnmod1i2  40448  atmod2i1  40449  atmod2i2  40450  atmod3i1  40452  atmod3i2  40453  atmod4i1  40454  atmod4i2  40455  llnexchb2lem  40456  llnexchb2  40457  dalawlem2  40460  dalawlem3  40461  dalawlem5  40463  dalawlem6  40464  dalawlem7  40465  dalawlem8  40466  dalawlem11  40469  dalawlem12  40470  polval2N  40494  pol1N  40498  polatN  40519  2polatN  40520  paddatclN  40537  linepsubclN  40539  lhp2lt  40589  lhp0lt  40591  lhpexle2lem  40597  lhpexle3lem  40599  lhpjat2  40609  lhpj1  40610  lhpmcvr3  40613  lhpmcvr4N  40614  lhpmcvr5N  40615  lhpmcvr6N  40616  lhpmatb  40619  lhp2at0  40620  lhp2atnle  40621  lhp2at0nle  40623  lhprelat3N  40628  lhple  40630  lhpat4N  40632  lhpat3  40634  4atexlemtlw  40655  4atexlemc  40657  4atexlemnclw  40658  4atexlemcnd  40660  4atex2-0aOLDN  40666  lauteq  40683  ltrnid  40723  ltrnel  40727  ltrnat  40728  ltrncnvat  40729  ltrncnvel  40730  ltrncoval  40733  ltrncnv  40734  ltrn11at  40735  ltrneq2  40736  ltrneq  40737  idltrn  40738  trlval2  40751  trlcnv  40753  trljat1  40754  trljat2  40755  ltrnideq  40763  arglem1N  40778  cdlemc1  40779  cdlemc2  40780  cdlemc4  40782  cdlemc5  40783  cdlemc6  40784  cdlemd1  40786  cdlemd2  40787  cdlemd3  40788  cdlemd4  40789  cdlemd7  40792  cdleme0aa  40798  cdleme0b  40800  cdleme0c  40801  cdleme0cp  40802  cdleme0cq  40803  cdleme0e  40805  cdleme0fN  40806  cdleme1b  40814  cdleme1  40815  cdleme2  40816  cdleme3b  40817  cdleme3c  40818  cdleme3e  40820  cdleme3g  40822  cdleme3h  40823  cdleme3  40825  cdleme5  40828  cdleme7d  40834  cdleme7e  40835  cdleme7ga  40836  cdleme7  40837  cdleme8  40838  cdleme9  40841  cdleme10  40842  cdleme11c  40849  cdleme11e  40851  cdleme11fN  40852  cdleme11g  40853  cdleme11k  40856  cdleme11  40858  cdleme15b  40863  cdleme15  40866  cdleme16b  40867  cdleme17b  40875  cdleme17c  40876  cdlemednpq  40887  cdleme20zN  40889  cdleme19a  40891  cdleme20bN  40898  cdleme20d  40900  cdleme20j  40906  cdleme21c  40915  cdleme22aa  40927  cdleme22b  40929  cdleme22cN  40930  cdleme22d  40931  cdleme22e  40932  cdleme22eALTN  40933  cdleme23b  40938  cdleme23c  40939  cdleme27N  40957  cdleme28a  40958  cdleme30a  40966  cdlemefrs29pre00  40983  cdlemefrs29bpre0  40984  cdlemefrs29cpre1  40986  cdlemefrs32fva  40988  cdlemefrs32fva1  40989  cdlemefr32snb  40993  cdlemefs32snb  41003  cdleme32snb  41024  cdleme32fva  41025  cdleme32fva1  41026  cdleme32fvaw  41027  cdleme35a  41036  cdleme35fnpq  41037  cdleme35b  41038  cdleme35c  41039  cdleme35f  41042  cdleme42c  41060  cdleme42e  41067  cdleme42h  41070  cdleme42i  41071  cdleme42ke  41073  cdleme42keg  41074  cdleme42mgN  41076  cdleme17d4  41085  cdleme48fvg  41088  cdleme48bw  41090  cdlemeg46req  41117  cdleme50trn3  41141  cdlemf1  41149  cdlemf2  41150  trlord  41157  ltrniotacnvval  41170  cdlemg2fv2  41188  cdlemg2l  41191  cdlemg7fvbwN  41195  cdlemg4c  41200  cdlemg4  41205  cdlemg6c  41208  cdlemg8b  41216  cdlemg11b  41230  cdlemg13a  41239  cdlemg17a  41249  cdlemg17h  41256  cdlemg17  41265  cdlemg18b  41267  cdlemg19a  41271  cdlemg27a  41280  cdlemg27b  41284  cdlemg31a  41285  cdlemg31b  41286  cdlemg31d  41288  cdlemg33b0  41289  cdlemg33a  41294  cdlemg35  41301  trlcolem  41314  cdlemg42  41317  cdlemg44a  41319  cdlemg46  41323  cdlemh1  41403  cdlemh2  41404  cdlemh  41405  cdlemi1  41406  cdlemi  41408  cdlemk3  41421  cdlemk4  41422  cdlemkvcl  41430  cdlemk7  41436  cdlemk11  41437  cdlemk15  41443  cdlemk1u  41447  cdlemk7u  41458  cdlemk11u  41459  cdlemk37  41502  cdlemk39  41504  cdlemkid1  41510  cdlemkid2  41512  cdlemk48  41538  cdlemk50  41540  cdlemk51  41541  cdlemk52  41542  dia2dimlem1  41652  dia2dimlem2  41653  dia2dimlem3  41654  dia2dimlem5  41656  dia2dimlem7  41658  dia2dimlem9  41660  dia2dimlem10  41661  dia2dimlem12  41663  dia2dimlem13  41664  cdlemm10N  41706  cdlemn2  41783  cdlemn3  41785  cdlemn9  41793  cdlemn10  41794  dihjustlem  41804  dihord1  41806  dihord2pre2  41814  dihvalcqat  41827  dib2dim  41831  dih2dimb  41832  dih2dimbALTN  41833  dihord5apre  41850  dihglbcpreN  41888  dihmeetlem3N  41893  dihmeetlem6  41897  dihjatc1  41899  dihjatc2N  41900  dihjatc3  41901  dihmeetlem9N  41903  dihmeetlem10N  41904  dihmeetlem11N  41905  dihmeetlem13N  41907  dihmeetlem15N  41909  dihmeetlem16N  41910  dihmeetlem17N  41911  dihatexv2  41927  dihjatb  42004  dihjatc  42005  dihjatcclem1  42006  dihjatcclem2  42007  dihjatcclem4  42009  dihjat  42011  dihjat3  42020  dihjat5N  42025  dvh4dimat  42026