Theorem atbase 39000

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  Vcvv 3462  ∅c0 4322   class class class wbr 5145  ‘cfv 6546  Basecbs 17208  0.cp0 18443   ⋖ ccvr 38973  Atomscatm 38974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pr 5425

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4323  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-br 5146  df-opab 5208  df-mpt 5229  df-id 5572  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-iota 6498  df-fun 6548  df-fv 6554  df-ats 38978

This theorem is referenced by:  atssbase  39001  0ltat  39002  leatb  39003  meetat  39007  atnle0  39020  atlen0  39021  atcmp  39022  atcvreq0  39025  atncvrN  39026  atnle  39028  atnem0  39029  atlatmstc  39030  atlatle  39031  cvlexch2  39040  cvlexchb1  39041  cvlexchb2  39042  cvlatexchb1  39045  cvlatexchb2  39046  cvlatexch1  39047  cvlatexch2  39048  cvlatexch3  39049  cvlcvr1  39050  cvlcvrp  39051  cvlatcvr1  39052  cvlatcvr2  39053  cvlsupr2  39054  cvlsupr7  39059  cvlsupr8  39060  hlatjcl  39078  hlatjcom  39079  hlatjidm  39080  hlatjass  39081  hlatj32  39083  hlatj4  39085  hlatlej1  39086  atnlej1  39091  atnlej2  39092  hlrelat5N  39113  hlrelat  39114  hlrelat2  39115  exatleN  39116  cvr2N  39123  hlrelat3  39124  cvrval3  39125  cvrval5  39127  cvrexchlem  39131  cvratlem  39133  cvrat  39134  atcvr0eq  39138  lnnat  39139  cvrat2  39141  atcvrneN  39142  atcvrj1  39143  atcvrj2b  39144  atltcvr  39147  atle  39148  atlelt  39150  2atlt  39151  atexchcvrN  39152  cvrat3  39154  cvrat4  39155  cvrat42  39156  2atjm  39157  atbtwn  39158  3noncolr2  39161  4noncolr3  39165  athgt  39168  3dim0  39169  3dimlem3a  39172  3dimlem3OLDN  39174  3dimlem4a  39175  3dimlem4OLDN  39177  3dim3  39181  2dim  39182  1cvratex  39185  1cvrjat  39187  1cvrat  39188  ps-1  39189  ps-2  39190  hlatexch3N  39192  hlatexch4  39193  ps-2b  39194  3atlem1  39195  3atlem2  39196  3atlem4  39198  3atlem5  39199  3atlem6  39200  3at  39202  islln3  39222  llnnleat  39225  llnn0  39228  llnle  39230  llnexatN  39233  llncmp  39234  2llnmat  39236  2at0mat0  39237  2atm  39239  ps-2c  39240  lplni2  39249  lplnle  39252  lplnnle2at  39253  lplnn0N  39259  islpln2a  39260  2atmat  39273  lplnexllnN  39276  2llnjaN  39278  2llnm4  39282  2llnmeqat  39283  lvoli3  39289  islvol5  39291  lvoli2  39293  lvolnle3at  39294  3atnelvolN  39298  lvoln0N  39303  islvol2aN  39304  4atlem3  39308  4atlem3a  39309  4atlem3b  39310  4atlem4a  39311  4atlem4b  39312  4atlem4c  39313  4atlem4d  39314  4atlem9  39315  4atlem10a  39316  4atlem10  39318  4atlem11a  39319  4atlem11b  39320  4atlem11  39321  4atlem12a  39322  4atlem12b  39323  4atlem12  39324  4at2  39326  lplncvrlvol2  39327  2lplnja  39331  dalempeb  39351  dalemqeb  39352  dalemreb  39353  dalemseb  39354  dalemteb  39355  dalemueb  39356  dalem3  39376  dalem16  39391  dalemcceb  39401  dalem21  39406  dalem25  39410  dalem38  39422  dalem39  39423  dalem43  39427  dalem44  39428  dalem45  39429  dalem53  39437  dalem54  39438  dalem55  39439  dalem57  39441  dalem60  39444  snatpsubN  39462  linepsubN  39464  pmaple  39473  pmapat  39475  pmap1N  39479  pmapsub  39480  pmapglbx  39481  isline2  39486  linepmap  39487  isline3  39488  isline4N  39489  lneq2at  39490  lncvrelatN  39493  lncmp  39495  2lnat  39496  2atm2atN  39497  2llnma1b  39498  2llnma1  39499  2llnma3r  39500  cdlema1N  39503  cdlemblem  39505  cdlemb  39506  elpaddn0  39512  paddcom  39525  paddasslem2  39533  paddasslem5  39536  paddasslem12  39543  paddasslem13  39544  pmapjoin  39564  pmapjat1  39565  pmapjat2  39566  pmapjlln1  39567  atmod1i1  39569  atmod1i2  39571  llnmod1i2  39572  atmod2i1  39573  atmod2i2  39574  atmod3i1  39576  atmod3i2  39577  atmod4i1  39578  atmod4i2  39579  llnexchb2lem  39580  llnexchb2  39581  dalawlem2  39584  dalawlem3  39585  dalawlem5  39587  dalawlem6  39588  dalawlem7  39589  dalawlem8  39590  dalawlem11  39593  dalawlem12  39594  polval2N  39618  pol1N  39622  polatN  39643  2polatN  39644  paddatclN  39661  linepsubclN  39663  lhp2lt  39713  lhp0lt  39715  lhpexle2lem  39721  lhpexle3lem  39723  lhpjat2  39733  lhpj1  39734  lhpmcvr3  39737  lhpmcvr4N  39738  lhpmcvr5N  39739  lhpmcvr6N  39740  lhpmatb  39743  lhp2at0  39744  lhp2atnle  39745  lhp2at0nle  39747  lhprelat3N  39752  lhple  39754  lhpat4N  39756  lhpat3  39758  4atexlemtlw  39779  4atexlemc  39781  4atexlemnclw  39782  4atexlemcnd  39784  4atex2-0aOLDN  39790  lauteq  39807  ltrnid  39847  ltrnel  39851  ltrnat  39852  ltrncnvat  39853  ltrncnvel  39854  ltrncoval  39857  ltrncnv  39858  ltrn11at  39859  ltrneq2  39860  ltrneq  39861  idltrn  39862  trlval2  39875  trlcnv  39877  trljat1  39878  trljat2  39879  ltrnideq  39887  arglem1N  39902  cdlemc1  39903  cdlemc2  39904  cdlemc4  39906  cdlemc5  39907  cdlemc6  39908  cdlemd1  39910  cdlemd2  39911  cdlemd3  39912  cdlemd4  39913  cdlemd7  39916  cdleme0aa  39922  cdleme0b  39924  cdleme0c  39925  cdleme0cp  39926  cdleme0cq  39927  cdleme0e  39929  cdleme0fN  39930  cdleme1b  39938  cdleme1  39939  cdleme2  39940  cdleme3b  39941  cdleme3c  39942  cdleme3e  39944  cdleme3g  39946  cdleme3h  39947  cdleme3  39949  cdleme5  39952  cdleme7d  39958  cdleme7e  39959  cdleme7ga  39960  cdleme7  39961  cdleme8  39962  cdleme9  39965  cdleme10  39966  cdleme11c  39973  cdleme11e  39975  cdleme11fN  39976  cdleme11g  39977  cdleme11k  39980  cdleme11  39982  cdleme15b  39987  cdleme15  39990  cdleme16b  39991  cdleme17b  39999  cdleme17c  40000  cdlemednpq  40011  cdleme20zN  40013  cdleme19a  40015  cdleme20bN  40022  cdleme20d  40024  cdleme20j  40030  cdleme21c  40039  cdleme22aa  40051  cdleme22b  40053  cdleme22cN  40054  cdleme22d  40055  cdleme22e  40056  cdleme22eALTN  40057  cdleme23b  40062  cdleme23c  40063  cdleme27N  40081  cdleme28a  40082  cdleme30a  40090  cdlemefrs29pre00  40107  cdlemefrs29bpre0  40108  cdlemefrs29cpre1  40110  cdlemefrs32fva  40112  cdlemefrs32fva1  40113  cdlemefr32snb  40117  cdlemefs32snb  40127  cdleme32snb  40148  cdleme32fva  40149  cdleme32fva1  40150  cdleme32fvaw  40151  cdleme35a  40160  cdleme35fnpq  40161  cdleme35b  40162  cdleme35c  40163  cdleme35f  40166  cdleme42c  40184  cdleme42e  40191  cdleme42h  40194  cdleme42i  40195  cdleme42ke  40197  cdleme42keg  40198  cdleme42mgN  40200  cdleme17d4  40209  cdleme48fvg  40212  cdleme48bw  40214  cdlemeg46req  40241  cdleme50trn3  40265  cdlemf1  40273  cdlemf2  40274  trlord  40281  ltrniotacnvval  40294  cdlemg2fv2  40312  cdlemg2l  40315  cdlemg7fvbwN  40319  cdlemg4c  40324  cdlemg4  40329  cdlemg6c  40332  cdlemg8b  40340  cdlemg11b  40354  cdlemg13a  40363  cdlemg17a  40373  cdlemg17h  40380  cdlemg17  40389  cdlemg18b  40391  cdlemg19a  40395  cdlemg27a  40404  cdlemg27b  40408  cdlemg31a  40409  cdlemg31b  40410  cdlemg31d  40412  cdlemg33b0  40413  cdlemg33a  40418  cdlemg35  40425  trlcolem  40438  cdlemg42  40441  cdlemg44a  40443  cdlemg46  40447  cdlemh1  40527  cdlemh2  40528  cdlemh  40529  cdlemi1  40530  cdlemi  40532  cdlemk3  40545  cdlemk4  40546  cdlemkvcl  40554  cdlemk7  40560  cdlemk11  40561  cdlemk15  40567  cdlemk1u  40571  cdlemk7u  40582  cdlemk11u  40583  cdlemk37  40626  cdlemk39  40628  cdlemkid1  40634  cdlemkid2  40636  cdlemk48  40662  cdlemk50  40664  cdlemk51  40665  cdlemk52  40666  dia2dimlem1  40776  dia2dimlem2  40777  dia2dimlem3  40778  dia2dimlem5  40780  dia2dimlem7  40782  dia2dimlem9  40784  dia2dimlem10  40785  dia2dimlem12  40787  dia2dimlem13  40788  cdlemm10N  40830  cdlemn2  40907  cdlemn3  40909  cdlemn9  40917  cdlemn10  40918  dihjustlem  40928  dihord1  40930  dihord2pre2  40938  dihvalcqat  40951  dib2dim  40955  dih2dimb  40956  dih2dimbALTN  40957  dihord5apre  40974  dihglbcpreN  41012  dihmeetlem3N  41017  dihmeetlem6  41021  dihjatc1  41023  dihjatc2N  41024  dihjatc3  41025  dihmeetlem9N  41027  dihmeetlem10N  41028  dihmeetlem11N  41029  dihmeetlem13N  41031  dihmeetlem15N  41033  dihmeetlem16N  41034  dihmeetlem17N  41035  dihatexv2  41051  dihjatb  41128  dihjatc  41129  dihjatcclem1  41130  dihjatcclem2  41131  dihjatcclem4  41133  dihjat  41135  dihjat3  41144  dihjat5N  41149  dvh4dimat  41150