Theorem atbase 39781

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  Vcvv 3431  ∅c0 4261   class class class wbr 5072  ‘cfv 6485  Basecbs 17170  0.cp0 18378   ⋖ ccvr 39754  Atomscatm 39755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-iota 6441  df-fun 6487  df-fv 6493  df-ats 39759

This theorem is referenced by:  atssbase  39782  0ltat  39783  leatb  39784  meetat  39788  atnle0  39801  atlen0  39802  atcmp  39803  atcvreq0  39806  atncvrN  39807  atnle  39809  atnem0  39810  atlatmstc  39811  atlatle  39812  cvlexch2  39821  cvlexchb1  39822  cvlexchb2  39823  cvlatexchb1  39826  cvlatexchb2  39827  cvlatexch1  39828  cvlatexch2  39829  cvlatexch3  39830  cvlcvr1  39831  cvlcvrp  39832  cvlatcvr1  39833  cvlatcvr2  39834  cvlsupr2  39835  cvlsupr7  39840  cvlsupr8  39841  hlatjcl  39859  hlatjcom  39860  hlatjidm  39861  hlatjass  39862  hlatj32  39864  hlatj4  39866  hlatlej1  39867  atnlej1  39871  atnlej2  39872  hlrelat5N  39893  hlrelat  39894  hlrelat2  39895  exatleN  39896  cvr2N  39903  hlrelat3  39904  cvrval3  39905  cvrval5  39907  cvrexchlem  39911  cvratlem  39913  cvrat  39914  atcvr0eq  39918  lnnat  39919  cvrat2  39921  atcvrneN  39922  atcvrj1  39923  atcvrj2b  39924  atltcvr  39927  atle  39928  atlelt  39930  2atlt  39931  atexchcvrN  39932  cvrat3  39934  cvrat4  39935  cvrat42  39936  2atjm  39937  atbtwn  39938  3noncolr2  39941  4noncolr3  39945  athgt  39948  3dim0  39949  3dimlem3a  39952  3dimlem3OLDN  39954  3dimlem4a  39955  3dimlem4OLDN  39957  3dim3  39961  2dim  39962  1cvratex  39965  1cvrjat  39967  1cvrat  39968  ps-1  39969  ps-2  39970  hlatexch3N  39972  hlatexch4  39973  ps-2b  39974  3atlem1  39975  3atlem2  39976  3atlem4  39978  3atlem5  39979  3atlem6  39980  3at  39982  islln3  40002  llnnleat  40005  llnn0  40008  llnle  40010  llnexatN  40013  llncmp  40014  2llnmat  40016  2at0mat0  40017  2atm  40019  ps-2c  40020  lplni2  40029  lplnle  40032  lplnnle2at  40033  lplnn0N  40039  islpln2a  40040  2atmat  40053  lplnexllnN  40056  2llnjaN  40058  2llnm4  40062  2llnmeqat  40063  lvoli3  40069  islvol5  40071  lvoli2  40073  lvolnle3at  40074  3atnelvolN  40078  lvoln0N  40083  islvol2aN  40084  4atlem3  40088  4atlem3a  40089  4atlem3b  40090  4atlem4a  40091  4atlem4b  40092  4atlem4c  40093  4atlem4d  40094  4atlem9  40095  4atlem10a  40096  4atlem10  40098  4atlem11a  40099  4atlem11b  40100  4atlem11  40101  4atlem12a  40102  4atlem12b  40103  4atlem12  40104  4at2  40106  lplncvrlvol2  40107  2lplnja  40111  dalempeb  40131  dalemqeb  40132  dalemreb  40133  dalemseb  40134  dalemteb  40135  dalemueb  40136  dalem3  40156  dalem16  40171  dalemcceb  40181  dalem21  40186  dalem25  40190  dalem38  40202  dalem39  40203  dalem43  40207  dalem44  40208  dalem45  40209  dalem53  40217  dalem54  40218  dalem55  40219  dalem57  40221  dalem60  40224  snatpsubN  40242  linepsubN  40244  pmaple  40253  pmapat  40255  pmap1N  40259  pmapsub  40260  pmapglbx  40261  isline2  40266  linepmap  40267  isline3  40268  isline4N  40269  lneq2at  40270  lncvrelatN  40273  lncmp  40275  2lnat  40276  2atm2atN  40277  2llnma1b  40278  2llnma1  40279  2llnma3r  40280  cdlema1N  40283  cdlemblem  40285  cdlemb  40286  elpaddn0  40292  paddcom  40305  paddasslem2  40313  paddasslem5  40316  paddasslem12  40323  paddasslem13  40324  pmapjoin  40344  pmapjat1  40345  pmapjat2  40346  pmapjlln1  40347  atmod1i1  40349  atmod1i2  40351  llnmod1i2  40352  atmod2i1  40353  atmod2i2  40354  atmod3i1  40356  atmod3i2  40357  atmod4i1  40358  atmod4i2  40359  llnexchb2lem  40360  llnexchb2  40361  dalawlem2  40364  dalawlem3  40365  dalawlem5  40367  dalawlem6  40368  dalawlem7  40369  dalawlem8  40370  dalawlem11  40373  dalawlem12  40374  polval2N  40398  pol1N  40402  polatN  40423  2polatN  40424  paddatclN  40441  linepsubclN  40443  lhp2lt  40493  lhp0lt  40495  lhpexle2lem  40501  lhpexle3lem  40503  lhpjat2  40513  lhpj1  40514  lhpmcvr3  40517  lhpmcvr4N  40518  lhpmcvr5N  40519  lhpmcvr6N  40520  lhpmatb  40523  lhp2at0  40524  lhp2atnle  40525  lhp2at0nle  40527  lhprelat3N  40532  lhple  40534  lhpat4N  40536  lhpat3  40538  4atexlemtlw  40559  4atexlemc  40561  4atexlemnclw  40562  4atexlemcnd  40564  4atex2-0aOLDN  40570  lauteq  40587  ltrnid  40627  ltrnel  40631  ltrnat  40632  ltrncnvat  40633  ltrncnvel  40634  ltrncoval  40637  ltrncnv  40638  ltrn11at  40639  ltrneq2  40640  ltrneq  40641  idltrn  40642  trlval2  40655  trlcnv  40657  trljat1  40658  trljat2  40659  ltrnideq  40667  arglem1N  40682  cdlemc1  40683  cdlemc2  40684  cdlemc4  40686  cdlemc5  40687  cdlemc6  40688  cdlemd1  40690  cdlemd2  40691  cdlemd3  40692  cdlemd4  40693  cdlemd7  40696  cdleme0aa  40702  cdleme0b  40704  cdleme0c  40705  cdleme0cp  40706  cdleme0cq  40707  cdleme0e  40709  cdleme0fN  40710  cdleme1b  40718  cdleme1  40719  cdleme2  40720  cdleme3b  40721  cdleme3c  40722  cdleme3e  40724  cdleme3g  40726  cdleme3h  40727  cdleme3  40729  cdleme5  40732  cdleme7d  40738  cdleme7e  40739  cdleme7ga  40740  cdleme7  40741  cdleme8  40742  cdleme9  40745  cdleme10  40746  cdleme11c  40753  cdleme11e  40755  cdleme11fN  40756  cdleme11g  40757  cdleme11k  40760  cdleme11  40762  cdleme15b  40767  cdleme15  40770  cdleme16b  40771  cdleme17b  40779  cdleme17c  40780  cdlemednpq  40791  cdleme20zN  40793  cdleme19a  40795  cdleme20bN  40802  cdleme20d  40804  cdleme20j  40810  cdleme21c  40819  cdleme22aa  40831  cdleme22b  40833  cdleme22cN  40834  cdleme22d  40835  cdleme22e  40836  cdleme22eALTN  40837  cdleme23b  40842  cdleme23c  40843  cdleme27N  40861  cdleme28a  40862  cdleme30a  40870  cdlemefrs29pre00  40887  cdlemefrs29bpre0  40888  cdlemefrs29cpre1  40890  cdlemefrs32fva  40892  cdlemefrs32fva1  40893  cdlemefr32snb  40897  cdlemefs32snb  40907  cdleme32snb  40928  cdleme32fva  40929  cdleme32fva1  40930  cdleme32fvaw  40931  cdleme35a  40940  cdleme35fnpq  40941  cdleme35b  40942  cdleme35c  40943  cdleme35f  40946  cdleme42c  40964  cdleme42e  40971  cdleme42h  40974  cdleme42i  40975  cdleme42ke  40977  cdleme42keg  40978  cdleme42mgN  40980  cdleme17d4  40989  cdleme48fvg  40992  cdleme48bw  40994  cdlemeg46req  41021  cdleme50trn3  41045  cdlemf1  41053  cdlemf2  41054  trlord  41061  ltrniotacnvval  41074  cdlemg2fv2  41092  cdlemg2l  41095  cdlemg7fvbwN  41099  cdlemg4c  41104  cdlemg4  41109  cdlemg6c  41112  cdlemg8b  41120  cdlemg11b  41134  cdlemg13a  41143  cdlemg17a  41153  cdlemg17h  41160  cdlemg17  41169  cdlemg18b  41171  cdlemg19a  41175  cdlemg27a  41184  cdlemg27b  41188  cdlemg31a  41189  cdlemg31b  41190  cdlemg31d  41192  cdlemg33b0  41193  cdlemg33a  41198  cdlemg35  41205  trlcolem  41218  cdlemg42  41221  cdlemg44a  41223  cdlemg46  41227  cdlemh1  41307  cdlemh2  41308  cdlemh  41309  cdlemi1  41310  cdlemi  41312  cdlemk3  41325  cdlemk4  41326  cdlemkvcl  41334  cdlemk7  41340  cdlemk11  41341  cdlemk15  41347  cdlemk1u  41351  cdlemk7u  41362  cdlemk11u  41363  cdlemk37  41406  cdlemk39  41408  cdlemkid1  41414  cdlemkid2  41416  cdlemk48  41442  cdlemk50  41444  cdlemk51  41445  cdlemk52  41446  dia2dimlem1  41556  dia2dimlem2  41557  dia2dimlem3  41558  dia2dimlem5  41560  dia2dimlem7  41562  dia2dimlem9  41564  dia2dimlem10  41565  dia2dimlem12  41567  dia2dimlem13  41568  cdlemm10N  41610  cdlemn2  41687  cdlemn3  41689  cdlemn9  41697  cdlemn10  41698  dihjustlem  41708  dihord1  41710  dihord2pre2  41718  dihvalcqat  41731  dib2dim  41735  dih2dimb  41736  dih2dimbALTN  41737  dihord5apre  41754  dihglbcpreN  41792  dihmeetlem3N  41797  dihmeetlem6  41801  dihjatc1  41803  dihjatc2N  41804  dihjatc3  41805  dihmeetlem9N  41807  dihmeetlem10N  41808  dihmeetlem11N  41809  dihmeetlem13N  41811  dihmeetlem15N  41813  dihmeetlem16N  41814  dihmeetlem17N  41815  dihatexv2  41831  dihjatb  41908  dihjatc  41909  dihjatcclem1  41910  dihjatcclem2  41911  dihjatcclem4  41913  dihjat  41915  dihjat3  41924  dihjat5N  41929  dvh4dimat  41930