Theorem atbase 36585

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 30127 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 4249	. . . 4 ⊢ (𝑃 ∈ 𝐴 → ¬ 𝐴 = ∅)
2		atombase.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
3	2	eqeq1i 2803	. . . 4 ⊢ (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
4	1, 3	sylnib 331	. . 3 ⊢ (𝑃 ∈ 𝐴 → ¬ (Atoms‘𝐾) = ∅)
5		fvprc 6638	. . 3 ⊢ (¬ 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
6	4, 5	nsyl2 143	. 2 ⊢ (𝑃 ∈ 𝐴 → 𝐾 ∈ V)
7		atombase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2798	. . . 4 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		eqid 2798	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	isat 36582	. . 3 ⊢ (𝐾 ∈ V → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
11	10	simprbda 502	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐵)
12	6, 11	mpancom 687	1 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  Vcvv 3441  ∅c0 4243   class class class wbr 5030  ‘cfv 6324  Basecbs 16475  0.cp0 17639   ⋖ ccvr 36558  Atomscatm 36559

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-iota 6283  df-fun 6326  df-fv 6332  df-ats 36563

This theorem is referenced by:  atssbase  36586  0ltat  36587  leatb  36588  meetat  36592  atnle0  36605  atlen0  36606  atcmp  36607  atcvreq0  36610  atncvrN  36611  atnle  36613  atnem0  36614  atlatmstc  36615  atlatle  36616  cvlexch2  36625  cvlexchb1  36626  cvlexchb2  36627  cvlatexchb1  36630  cvlatexchb2  36631  cvlatexch1  36632  cvlatexch2  36633  cvlatexch3  36634  cvlcvr1  36635  cvlcvrp  36636  cvlatcvr1  36637  cvlatcvr2  36638  cvlsupr2  36639  cvlsupr7  36644  cvlsupr8  36645  hlatjcl  36663  hlatjcom  36664  hlatjidm  36665  hlatjass  36666  hlatj32  36668  hlatj4  36670  hlatlej1  36671  atnlej1  36675  atnlej2  36676  hlrelat5N  36697  hlrelat  36698  hlrelat2  36699  exatleN  36700  cvr2N  36707  hlrelat3  36708  cvrval3  36709  cvrval5  36711  cvrexchlem  36715  cvratlem  36717  cvrat  36718  atcvr0eq  36722  lnnat  36723  cvrat2  36725  atcvrneN  36726  atcvrj1  36727  atcvrj2b  36728  atltcvr  36731  atle  36732  atlelt  36734  2atlt  36735  atexchcvrN  36736  cvrat3  36738  cvrat4  36739  cvrat42  36740  2atjm  36741  atbtwn  36742  3noncolr2  36745  4noncolr3  36749  athgt  36752  3dim0  36753  3dimlem3a  36756  3dimlem3OLDN  36758  3dimlem4a  36759  3dimlem4OLDN  36761  3dim3  36765  2dim  36766  1cvratex  36769  1cvrjat  36771  1cvrat  36772  ps-1  36773  ps-2  36774  hlatexch3N  36776  hlatexch4  36777  ps-2b  36778  3atlem1  36779  3atlem2  36780  3atlem4  36782  3atlem5  36783  3atlem6  36784  3at  36786  islln3  36806  llnnleat  36809  llnn0  36812  llnle  36814  llnexatN  36817  llncmp  36818  2llnmat  36820  2at0mat0  36821  2atm  36823  ps-2c  36824  lplni2  36833  lplnle  36836  lplnnle2at  36837  lplnn0N  36843  islpln2a  36844  2atmat  36857  lplnexllnN  36860  2llnjaN  36862  2llnm4  36866  2llnmeqat  36867  lvoli3  36873  islvol5  36875  lvoli2  36877  lvolnle3at  36878  3atnelvolN  36882  lvoln0N  36887  islvol2aN  36888  4atlem3  36892  4atlem3a  36893  4atlem3b  36894  4atlem4a  36895  4atlem4b  36896  4atlem4c  36897  4atlem4d  36898  4atlem9  36899  4atlem10a  36900  4atlem10  36902  4atlem11a  36903  4atlem11b  36904  4atlem11  36905  4atlem12a  36906  4atlem12b  36907  4atlem12  36908  4at2  36910  lplncvrlvol2  36911  2lplnja  36915  dalempeb  36935  dalemqeb  36936  dalemreb  36937  dalemseb  36938  dalemteb  36939  dalemueb  36940  dalem3  36960  dalem16  36975  dalemcceb  36985  dalem21  36990  dalem25  36994  dalem38  37006  dalem39  37007  dalem43  37011  dalem44  37012  dalem45  37013  dalem53  37021  dalem54  37022  dalem55  37023  dalem57  37025  dalem60  37028  snatpsubN  37046  linepsubN  37048  pmaple  37057  pmapat  37059  pmap1N  37063  pmapsub  37064  pmapglbx  37065  isline2  37070  linepmap  37071  isline3  37072  isline4N  37073  lneq2at  37074  lncvrelatN  37077  lncmp  37079  2lnat  37080  2atm2atN  37081  2llnma1b  37082  2llnma1  37083  2llnma3r  37084  cdlema1N  37087  cdlemblem  37089  cdlemb  37090  elpaddn0  37096  paddcom  37109  paddasslem2  37117  paddasslem5  37120  paddasslem12  37127  paddasslem13  37128  pmapjoin  37148  pmapjat1  37149  pmapjat2  37150  pmapjlln1  37151  atmod1i1  37153  atmod1i2  37155  llnmod1i2  37156  atmod2i1  37157  atmod2i2  37158  atmod3i1  37160  atmod3i2  37161  atmod4i1  37162  atmod4i2  37163  llnexchb2lem  37164  llnexchb2  37165  dalawlem2  37168  dalawlem3  37169  dalawlem5  37171  dalawlem6  37172  dalawlem7  37173  dalawlem8  37174  dalawlem11  37177  dalawlem12  37178  polval2N  37202  pol1N  37206  polatN  37227  2polatN  37228  paddatclN  37245  linepsubclN  37247  lhp2lt  37297  lhp0lt  37299  lhpexle2lem  37305  lhpexle3lem  37307  lhpjat2  37317  lhpj1  37318  lhpmcvr3  37321  lhpmcvr4N  37322  lhpmcvr5N  37323  lhpmcvr6N  37324  lhpmatb  37327  lhp2at0  37328  lhp2atnle  37329  lhp2at0nle  37331  lhprelat3N  37336  lhple  37338  lhpat4N  37340  lhpat3  37342  4atexlemtlw  37363  4atexlemc  37365  4atexlemnclw  37366  4atexlemcnd  37368  4atex2-0aOLDN  37374  lauteq  37391  ltrnid  37431  ltrnel  37435  ltrnat  37436  ltrncnvat  37437  ltrncnvel  37438  ltrncoval  37441  ltrncnv  37442  ltrn11at  37443  ltrneq2  37444  ltrneq  37445  idltrn  37446  trlval2  37459  trlcnv  37461  trljat1  37462  trljat2  37463  ltrnideq  37471  arglem1N  37486  cdlemc1  37487  cdlemc2  37488  cdlemc4  37490  cdlemc5  37491  cdlemc6  37492  cdlemd1  37494  cdlemd2  37495  cdlemd3  37496  cdlemd4  37497  cdlemd7  37500  cdleme0aa  37506  cdleme0b  37508  cdleme0c  37509  cdleme0cp  37510  cdleme0cq  37511  cdleme0e  37513  cdleme0fN  37514  cdleme1b  37522  cdleme1  37523  cdleme2  37524  cdleme3b  37525  cdleme3c  37526  cdleme3e  37528  cdleme3g  37530  cdleme3h  37531  cdleme3  37533  cdleme5  37536  cdleme7d  37542  cdleme7e  37543  cdleme7ga  37544  cdleme7  37545  cdleme8  37546  cdleme9  37549  cdleme10  37550  cdleme11c  37557  cdleme11e  37559  cdleme11fN  37560  cdleme11g  37561  cdleme11k  37564  cdleme11  37566  cdleme15b  37571  cdleme15  37574  cdleme16b  37575  cdleme17b  37583  cdleme17c  37584  cdlemednpq  37595  cdleme20zN  37597  cdleme19a  37599  cdleme20bN  37606  cdleme20d  37608  cdleme20j  37614  cdleme21c  37623  cdleme22aa  37635  cdleme22b  37637  cdleme22cN  37638  cdleme22d  37639  cdleme22e  37640  cdleme22eALTN  37641  cdleme23b  37646  cdleme23c  37647  cdleme27N  37665  cdleme28a  37666  cdleme30a  37674  cdlemefrs29pre00  37691  cdlemefrs29bpre0  37692  cdlemefrs29cpre1  37694  cdlemefrs32fva  37696  cdlemefrs32fva1  37697  cdlemefr32snb  37701  cdlemefs32snb  37711  cdleme32snb  37732  cdleme32fva  37733  cdleme32fva1  37734  cdleme32fvaw  37735  cdleme35a  37744  cdleme35fnpq  37745  cdleme35b  37746  cdleme35c  37747  cdleme35f  37750  cdleme42c  37768  cdleme42e  37775  cdleme42h  37778  cdleme42i  37779  cdleme42ke  37781  cdleme42keg  37782  cdleme42mgN  37784  cdleme17d4  37793  cdleme48fvg  37796  cdleme48bw  37798  cdlemeg46req  37825  cdleme50trn3  37849  cdlemf1  37857  cdlemf2  37858  trlord  37865  ltrniotacnvval  37878  cdlemg2fv2  37896  cdlemg2l  37899  cdlemg7fvbwN  37903  cdlemg4c  37908  cdlemg4  37913  cdlemg6c  37916  cdlemg8b  37924  cdlemg11b  37938  cdlemg13a  37947  cdlemg17a  37957  cdlemg17h  37964  cdlemg17  37973  cdlemg18b  37975  cdlemg19a  37979  cdlemg27a  37988  cdlemg27b  37992  cdlemg31a  37993  cdlemg31b  37994  cdlemg31d  37996  cdlemg33b0  37997  cdlemg33a  38002  cdlemg35  38009  trlcolem  38022  cdlemg42  38025  cdlemg44a  38027  cdlemg46  38031  cdlemh1  38111  cdlemh2  38112  cdlemh  38113  cdlemi1  38114  cdlemi  38116  cdlemk3  38129  cdlemk4  38130  cdlemkvcl  38138  cdlemk7  38144  cdlemk11  38145  cdlemk15  38151  cdlemk1u  38155  cdlemk7u  38166  cdlemk11u  38167  cdlemk37  38210  cdlemk39  38212  cdlemkid1  38218  cdlemkid2  38220  cdlemk48  38246  cdlemk50  38248  cdlemk51  38249  cdlemk52  38250  dia2dimlem1  38360  dia2dimlem2  38361  dia2dimlem3  38362  dia2dimlem5  38364  dia2dimlem7  38366  dia2dimlem9  38368  dia2dimlem10  38369  dia2dimlem12  38371  dia2dimlem13  38372  cdlemm10N  38414  cdlemn2  38491  cdlemn3  38493  cdlemn9  38501  cdlemn10  38502  dihjustlem  38512  dihord1  38514  dihord2pre2  38522  dihvalcqat  38535  dib2dim  38539  dih2dimb  38540  dih2dimbALTN  38541  dihord5apre  38558  dihglbcpreN  38596  dihmeetlem3N  38601  dihmeetlem6  38605  dihjatc1  38607  dihjatc2N  38608  dihjatc3  38609  dihmeetlem9N  38611  dihmeetlem10N  38612  dihmeetlem11N  38613  dihmeetlem13N  38615  dihmeetlem15N  38617  dihmeetlem16N  38618  dihmeetlem17N  38619  dihatexv2  38635  dihjatb  38712  dihjatc  38713  dihjatcclem1  38714  dihjatcclem2  38715  dihjatcclem4  38717  dihjat  38719  dihjat3  38728  dihjat5N  38733  dvh4dimat  38734