Theorem atbase 39245

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  Vcvv 3488  ∅c0 4352   class class class wbr 5166  ‘cfv 6573  Basecbs 17258  0.cp0 18493   ⋖ ccvr 39218  Atomscatm 39219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-iota 6525  df-fun 6575  df-fv 6581  df-ats 39223

This theorem is referenced by:  atssbase  39246  0ltat  39247  leatb  39248  meetat  39252  atnle0  39265  atlen0  39266  atcmp  39267  atcvreq0  39270  atncvrN  39271  atnle  39273  atnem0  39274  atlatmstc  39275  atlatle  39276  cvlexch2  39285  cvlexchb1  39286  cvlexchb2  39287  cvlatexchb1  39290  cvlatexchb2  39291  cvlatexch1  39292  cvlatexch2  39293  cvlatexch3  39294  cvlcvr1  39295  cvlcvrp  39296  cvlatcvr1  39297  cvlatcvr2  39298  cvlsupr2  39299  cvlsupr7  39304  cvlsupr8  39305  hlatjcl  39323  hlatjcom  39324  hlatjidm  39325  hlatjass  39326  hlatj32  39328  hlatj4  39330  hlatlej1  39331  atnlej1  39336  atnlej2  39337  hlrelat5N  39358  hlrelat  39359  hlrelat2  39360  exatleN  39361  cvr2N  39368  hlrelat3  39369  cvrval3  39370  cvrval5  39372  cvrexchlem  39376  cvratlem  39378  cvrat  39379  atcvr0eq  39383  lnnat  39384  cvrat2  39386  atcvrneN  39387  atcvrj1  39388  atcvrj2b  39389  atltcvr  39392  atle  39393  atlelt  39395  2atlt  39396  atexchcvrN  39397  cvrat3  39399  cvrat4  39400  cvrat42  39401  2atjm  39402  atbtwn  39403  3noncolr2  39406  4noncolr3  39410  athgt  39413  3dim0  39414  3dimlem3a  39417  3dimlem3OLDN  39419  3dimlem4a  39420  3dimlem4OLDN  39422  3dim3  39426  2dim  39427  1cvratex  39430  1cvrjat  39432  1cvrat  39433  ps-1  39434  ps-2  39435  hlatexch3N  39437  hlatexch4  39438  ps-2b  39439  3atlem1  39440  3atlem2  39441  3atlem4  39443  3atlem5  39444  3atlem6  39445  3at  39447  islln3  39467  llnnleat  39470  llnn0  39473  llnle  39475  llnexatN  39478  llncmp  39479  2llnmat  39481  2at0mat0  39482  2atm  39484  ps-2c  39485  lplni2  39494  lplnle  39497  lplnnle2at  39498  lplnn0N  39504  islpln2a  39505  2atmat  39518  lplnexllnN  39521  2llnjaN  39523  2llnm4  39527  2llnmeqat  39528  lvoli3  39534  islvol5  39536  lvoli2  39538  lvolnle3at  39539  3atnelvolN  39543  lvoln0N  39548  islvol2aN  39549  4atlem3  39553  4atlem3a  39554  4atlem3b  39555  4atlem4a  39556  4atlem4b  39557  4atlem4c  39558  4atlem4d  39559  4atlem9  39560  4atlem10a  39561  4atlem10  39563  4atlem11a  39564  4atlem11b  39565  4atlem11  39566  4atlem12a  39567  4atlem12b  39568  4atlem12  39569  4at2  39571  lplncvrlvol2  39572  2lplnja  39576  dalempeb  39596  dalemqeb  39597  dalemreb  39598  dalemseb  39599  dalemteb  39600  dalemueb  39601  dalem3  39621  dalem16  39636  dalemcceb  39646  dalem21  39651  dalem25  39655  dalem38  39667  dalem39  39668  dalem43  39672  dalem44  39673  dalem45  39674  dalem53  39682  dalem54  39683  dalem55  39684  dalem57  39686  dalem60  39689  snatpsubN  39707  linepsubN  39709  pmaple  39718  pmapat  39720  pmap1N  39724  pmapsub  39725  pmapglbx  39726  isline2  39731  linepmap  39732  isline3  39733  isline4N  39734  lneq2at  39735  lncvrelatN  39738  lncmp  39740  2lnat  39741  2atm2atN  39742  2llnma1b  39743  2llnma1  39744  2llnma3r  39745  cdlema1N  39748  cdlemblem  39750  cdlemb  39751  elpaddn0  39757  paddcom  39770  paddasslem2  39778  paddasslem5  39781  paddasslem12  39788  paddasslem13  39789  pmapjoin  39809  pmapjat1  39810  pmapjat2  39811  pmapjlln1  39812  atmod1i1  39814  atmod1i2  39816  llnmod1i2  39817  atmod2i1  39818  atmod2i2  39819  atmod3i1  39821  atmod3i2  39822  atmod4i1  39823  atmod4i2  39824  llnexchb2lem  39825  llnexchb2  39826  dalawlem2  39829  dalawlem3  39830  dalawlem5  39832  dalawlem6  39833  dalawlem7  39834  dalawlem8  39835  dalawlem11  39838  dalawlem12  39839  polval2N  39863  pol1N  39867  polatN  39888  2polatN  39889  paddatclN  39906  linepsubclN  39908  lhp2lt  39958  lhp0lt  39960  lhpexle2lem  39966  lhpexle3lem  39968  lhpjat2  39978  lhpj1  39979  lhpmcvr3  39982  lhpmcvr4N  39983  lhpmcvr5N  39984  lhpmcvr6N  39985  lhpmatb  39988  lhp2at0  39989  lhp2atnle  39990  lhp2at0nle  39992  lhprelat3N  39997  lhple  39999  lhpat4N  40001  lhpat3  40003  4atexlemtlw  40024  4atexlemc  40026  4atexlemnclw  40027  4atexlemcnd  40029  4atex2-0aOLDN  40035  lauteq  40052  ltrnid  40092  ltrnel  40096  ltrnat  40097  ltrncnvat  40098  ltrncnvel  40099  ltrncoval  40102  ltrncnv  40103  ltrn11at  40104  ltrneq2  40105  ltrneq  40106  idltrn  40107  trlval2  40120  trlcnv  40122  trljat1  40123  trljat2  40124  ltrnideq  40132  arglem1N  40147  cdlemc1  40148  cdlemc2  40149  cdlemc4  40151  cdlemc5  40152  cdlemc6  40153  cdlemd1  40155  cdlemd2  40156  cdlemd3  40157  cdlemd4  40158  cdlemd7  40161  cdleme0aa  40167  cdleme0b  40169  cdleme0c  40170  cdleme0cp  40171  cdleme0cq  40172  cdleme0e  40174  cdleme0fN  40175  cdleme1b  40183  cdleme1  40184  cdleme2  40185  cdleme3b  40186  cdleme3c  40187  cdleme3e  40189  cdleme3g  40191  cdleme3h  40192  cdleme3  40194  cdleme5  40197  cdleme7d  40203  cdleme7e  40204  cdleme7ga  40205  cdleme7  40206  cdleme8  40207  cdleme9  40210  cdleme10  40211  cdleme11c  40218  cdleme11e  40220  cdleme11fN  40221  cdleme11g  40222  cdleme11k  40225  cdleme11  40227  cdleme15b  40232  cdleme15  40235  cdleme16b  40236  cdleme17b  40244  cdleme17c  40245  cdlemednpq  40256  cdleme20zN  40258  cdleme19a  40260  cdleme20bN  40267  cdleme20d  40269  cdleme20j  40275  cdleme21c  40284  cdleme22aa  40296  cdleme22b  40298  cdleme22cN  40299  cdleme22d  40300  cdleme22e  40301  cdleme22eALTN  40302  cdleme23b  40307  cdleme23c  40308  cdleme27N  40326  cdleme28a  40327  cdleme30a  40335  cdlemefrs29pre00  40352  cdlemefrs29bpre0  40353  cdlemefrs29cpre1  40355  cdlemefrs32fva  40357  cdlemefrs32fva1  40358  cdlemefr32snb  40362  cdlemefs32snb  40372  cdleme32snb  40393  cdleme32fva  40394  cdleme32fva1  40395  cdleme32fvaw  40396  cdleme35a  40405  cdleme35fnpq  40406  cdleme35b  40407  cdleme35c  40408  cdleme35f  40411  cdleme42c  40429  cdleme42e  40436  cdleme42h  40439  cdleme42i  40440  cdleme42ke  40442  cdleme42keg  40443  cdleme42mgN  40445  cdleme17d4  40454  cdleme48fvg  40457  cdleme48bw  40459  cdlemeg46req  40486  cdleme50trn3  40510  cdlemf1  40518  cdlemf2  40519  trlord  40526  ltrniotacnvval  40539  cdlemg2fv2  40557  cdlemg2l  40560  cdlemg7fvbwN  40564  cdlemg4c  40569  cdlemg4  40574  cdlemg6c  40577  cdlemg8b  40585  cdlemg11b  40599  cdlemg13a  40608  cdlemg17a  40618  cdlemg17h  40625  cdlemg17  40634  cdlemg18b  40636  cdlemg19a  40640  cdlemg27a  40649  cdlemg27b  40653  cdlemg31a  40654  cdlemg31b  40655  cdlemg31d  40657  cdlemg33b0  40658  cdlemg33a  40663  cdlemg35  40670  trlcolem  40683  cdlemg42  40686  cdlemg44a  40688  cdlemg46  40692  cdlemh1  40772  cdlemh2  40773  cdlemh  40774  cdlemi1  40775  cdlemi  40777  cdlemk3  40790  cdlemk4  40791  cdlemkvcl  40799  cdlemk7  40805  cdlemk11  40806  cdlemk15  40812  cdlemk1u  40816  cdlemk7u  40827  cdlemk11u  40828  cdlemk37  40871  cdlemk39  40873  cdlemkid1  40879  cdlemkid2  40881  cdlemk48  40907  cdlemk50  40909  cdlemk51  40910  cdlemk52  40911  dia2dimlem1  41021  dia2dimlem2  41022  dia2dimlem3  41023  dia2dimlem5  41025  dia2dimlem7  41027  dia2dimlem9  41029  dia2dimlem10  41030  dia2dimlem12  41032  dia2dimlem13  41033  cdlemm10N  41075  cdlemn2  41152  cdlemn3  41154  cdlemn9  41162  cdlemn10  41163  dihjustlem  41173  dihord1  41175  dihord2pre2  41183  dihvalcqat  41196  dib2dim  41200  dih2dimb  41201  dih2dimbALTN  41202  dihord5apre  41219  dihglbcpreN  41257  dihmeetlem3N  41262  dihmeetlem6  41266  dihjatc1  41268  dihjatc2N  41269  dihjatc3  41270  dihmeetlem9N  41272  dihmeetlem10N  41273  dihmeetlem11N  41274  dihmeetlem13N  41276  dihmeetlem15N  41278  dihmeetlem16N  41279  dihmeetlem17N  41280  dihatexv2  41296  dihjatb  41373  dihjatc  41374  dihjatcclem1  41375  dihjatcclem2  41376  dihjatcclem4  41378  dihjat  41380  dihjat3  41389  dihjat5N  41394  dvh4dimat  41395