Theorem atbase 40314

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  Vcvv 3451  ∅c0 4279   class class class wbr 5103  ‘cfv 6531  Basecbs 17367  0.cp0 18575   ⋖ ccvr 40287  Atomscatm 40288

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6487  df-fun 6533  df-fv 6539  df-ats 40292

This theorem is used by:  atssbase  40315  0ltat  40316  leatb  40317  meetat  40321  atnle0  40334  atlen0  40335  atcmp  40336  atcvreq0  40339  atncvrN  40340  atnle  40342  atnem0  40343  atlatmstc  40344  atlatle  40345  cvlexch2  40354  cvlexchb1  40355  cvlexchb2  40356  cvlatexchb1  40359  cvlatexchb2  40360  cvlatexch1  40361  cvlatexch2  40362  cvlatexch3  40363  cvlcvr1  40364  cvlcvrp  40365  cvlatcvr1  40366  cvlatcvr2  40367  cvlsupr2  40368  cvlsupr7  40373  cvlsupr8  40374  hlatjcl  40392  hlatjcom  40393  hlatjidm  40394  hlatjass  40395  hlatj32  40397  hlatj4  40399  hlatlej1  40400  atnlej1  40404  atnlej2  40405  hlrelat5N  40426  hlrelat  40427  hlrelat2  40428  exatleN  40429  cvr2N  40436  hlrelat3  40437  cvrval3  40438  cvrval5  40440  cvrexchlem  40444  cvratlem  40446  cvrat  40447  atcvr0eq  40451  lnnat  40452  cvrat2  40454  atcvrneN  40455  atcvrj1  40456  atcvrj2b  40457  atltcvr  40460  atle  40461  atlelt  40463  2atlt  40464  atexchcvrN  40465  cvrat3  40467  cvrat4  40468  cvrat42  40469  2atjm  40470  atbtwn  40471  3noncolr2  40474  4noncolr3  40478  athgt  40481  3dim0  40482  3dimlem3a  40485  3dimlem3OLDN  40487  3dimlem4a  40488  3dimlem4OLDN  40490  3dim3  40494  2dim  40495  1cvratex  40498  1cvrjat  40500  1cvrat  40501  ps-1  40502  ps-2  40503  hlatexch3N  40505  hlatexch4  40506  ps-2b  40507  3atlem1  40508  3atlem2  40509  3atlem4  40511  3atlem5  40512  3atlem6  40513  3at  40515  islln3  40535  llnnleat  40538  llnn0  40541  llnle  40543  llnexatN  40546  llncmp  40547  2llnmat  40549  2at0mat0  40550  2atm  40552  ps-2c  40553  lplni2  40562  lplnle  40565  lplnnle2at  40566  lplnn0N  40572  islpln2a  40573  2atmat  40586  lplnexllnN  40589  2llnjaN  40591  2llnm4  40595  2llnmeqat  40596  lvoli3  40602  islvol5  40604  lvoli2  40606  lvolnle3at  40607  3atnelvolN  40611  lvoln0N  40616  islvol2aN  40617  4atlem3  40621  4atlem3a  40622  4atlem3b  40623  4atlem4a  40624  4atlem4b  40625  4atlem4c  40626  4atlem4d  40627  4atlem9  40628  4atlem10a  40629  4atlem10  40631  4atlem11a  40632  4atlem11b  40633  4atlem11  40634  4atlem12a  40635  4atlem12b  40636  4atlem12  40637  4at2  40639  lplncvrlvol2  40640  2lplnja  40644  dalempeb  40664  dalemqeb  40665  dalemreb  40666  dalemseb  40667  dalemteb  40668  dalemueb  40669  dalem3  40689  dalem16  40704  dalemcceb  40714  dalem21  40719  dalem25  40723  dalem38  40735  dalem39  40736  dalem43  40740  dalem44  40741  dalem45  40742  dalem53  40750  dalem54  40751  dalem55  40752  dalem57  40754  dalem60  40757  snatpsubN  40775  linepsubN  40777  pmaple  40786  pmapat  40788  pmap1N  40792  pmapsub  40793  pmapglbx  40794  isline2  40799  linepmap  40800  isline3  40801  isline4N  40802  lneq2at  40803  lncvrelatN  40806  lncmp  40808  2lnat  40809  2atm2atN  40810  2llnma1b  40811  2llnma1  40812  2llnma3r  40813  cdlema1N  40816  cdlemblem  40818  cdlemb  40819  elpaddn0  40825  paddcom  40838  paddasslem2  40846  paddasslem5  40849  paddasslem12  40856  paddasslem13  40857  pmapjoin  40877  pmapjat1  40878  pmapjat2  40879  pmapjlln1  40880  atmod1i1  40882  atmod1i2  40884  llnmod1i2  40885  atmod2i1  40886  atmod2i2  40887  atmod3i1  40889  atmod3i2  40890  atmod4i1  40891  atmod4i2  40892  llnexchb2lem  40893  llnexchb2  40894  dalawlem2  40897  dalawlem3  40898  dalawlem5  40900  dalawlem6  40901  dalawlem7  40902  dalawlem8  40903  dalawlem11  40906  dalawlem12  40907  polval2N  40931  pol1N  40935  polatN  40956  2polatN  40957  paddatclN  40974  linepsubclN  40976  lhp2lt  41026  lhp0lt  41028  lhpexle2lem  41034  lhpexle3lem  41036  lhpjat2  41046  lhpj1  41047  lhpmcvr3  41050  lhpmcvr4N  41051  lhpmcvr5N  41052  lhpmcvr6N  41053  lhpmatb  41056  lhp2at0  41057  lhp2atnle  41058  lhp2at0nle  41060  lhprelat3N  41065  lhple  41067  lhpat4N  41069  lhpat3  41071  4atexlemtlw  41092  4atexlemc  41094  4atexlemnclw  41095  4atexlemcnd  41097  4atex2-0aOLDN  41103  lauteq  41120  ltrnid  41160  ltrnel  41164  ltrnat  41165  ltrncnvat  41166  ltrncnvel  41167  ltrncoval  41170  ltrncnv  41171  ltrn11at  41172  ltrneq2  41173  ltrneq  41174  idltrn  41175  trlval2  41188  trlcnv  41190  trljat1  41191  trljat2  41192  ltrnideq  41200  arglem1N  41215  cdlemc1  41216  cdlemc2  41217  cdlemc4  41219  cdlemc5  41220  cdlemc6  41221  cdlemd1  41223  cdlemd2  41224  cdlemd3  41225  cdlemd4  41226  cdlemd7  41229  cdleme0aa  41235  cdleme0b  41237  cdleme0c  41238  cdleme0cp  41239  cdleme0cq  41240  cdleme0e  41242  cdleme0fN  41243  cdleme1b  41251  cdleme1  41252  cdleme2  41253  cdleme3b  41254  cdleme3c  41255  cdleme3e  41257  cdleme3g  41259  cdleme3h  41260  cdleme3  41262  cdleme5  41265  cdleme7d  41271  cdleme7e  41272  cdleme7ga  41273  cdleme7  41274  cdleme8  41275  cdleme9  41278  cdleme10  41279  cdleme11c  41286  cdleme11e  41288  cdleme11fN  41289  cdleme11g  41290  cdleme11k  41293  cdleme11  41295  cdleme15b  41300  cdleme15  41303  cdleme16b  41304  cdleme17b  41312  cdleme17c  41313  cdlemednpq  41324  cdleme20zN  41326  cdleme19a  41328  cdleme20bN  41335  cdleme20d  41337  cdleme20j  41343  cdleme21c  41352  cdleme22aa  41364  cdleme22b  41366  cdleme22cN  41367  cdleme22d  41368  cdleme22e  41369  cdleme22eALTN  41370  cdleme23b  41375  cdleme23c  41376  cdleme27N  41394  cdleme28a  41395  cdleme30a  41403  cdlemefrs29pre00  41420  cdlemefrs29bpre0  41421  cdlemefrs29cpre1  41423  cdlemefrs32fva  41425  cdlemefrs32fva1  41426  cdlemefr32snb  41430  cdlemefs32snb  41440  cdleme32snb  41461  cdleme32fva  41462  cdleme32fva1  41463  cdleme32fvaw  41464  cdleme35a  41473  cdleme35fnpq  41474  cdleme35b  41475  cdleme35c  41476  cdleme35f  41479  cdleme42c  41497  cdleme42e  41504  cdleme42h  41507  cdleme42i  41508  cdleme42ke  41510  cdleme42keg  41511  cdleme42mgN  41513  cdleme17d4  41522  cdleme48fvg  41525  cdleme48bw  41527  cdlemeg46req  41554  cdleme50trn3  41578  cdlemf1  41586  cdlemf2  41587  trlord  41594  ltrniotacnvval  41607  cdlemg2fv2  41625  cdlemg2l  41628  cdlemg7fvbwN  41632  cdlemg4c  41637  cdlemg4  41642  cdlemg6c  41645  cdlemg8b  41653  cdlemg11b  41667  cdlemg13a  41676  cdlemg17a  41686  cdlemg17h  41693  cdlemg17  41702  cdlemg18b  41704  cdlemg19a  41708  cdlemg27a  41717  cdlemg27b  41721  cdlemg31a  41722  cdlemg31b  41723  cdlemg31d  41725  cdlemg33b0  41726  cdlemg33a  41731  cdlemg35  41738  trlcolem  41751  cdlemg42  41754  cdlemg44a  41756  cdlemg46  41760  cdlemh1  41840  cdlemh2  41841  cdlemh  41842  cdlemi1  41843  cdlemi  41845  cdlemk3  41858  cdlemk4  41859  cdlemkvcl  41867  cdlemk7  41873  cdlemk11  41874  cdlemk15  41880  cdlemk1u  41884  cdlemk7u  41895  cdlemk11u  41896  cdlemk37  41939  cdlemk39  41941  cdlemkid1  41947  cdlemkid2  41949  cdlemk48  41975  cdlemk50  41977  cdlemk51  41978  cdlemk52  41979  dia2dimlem1  42089  dia2dimlem2  42090  dia2dimlem3  42091  dia2dimlem5  42093  dia2dimlem7  42095  dia2dimlem9  42097  dia2dimlem10  42098  dia2dimlem12  42100  dia2dimlem13  42101  cdlemm10N  42143  cdlemn2  42220  cdlemn3  42222  cdlemn9  42230  cdlemn10  42231  dihjustlem  42241  dihord1  42243  dihord2pre2  42251  dihvalcqat  42264  dib2dim  42268  dih2dimb  42269  dih2dimbALTN  42270  dihord5apre  42287  dihglbcpreN  42325  dihmeetlem3N  42330  dihmeetlem6  42334  dihjatc1  42336  dihjatc2N  42337  dihjatc3  42338  dihmeetlem9N  42340  dihmeetlem10N  42341  dihmeetlem11N  42342  dihmeetlem13N  42344  dihmeetlem15N  42346  dihmeetlem16N  42347  dihmeetlem17N  42348  dihatexv2  42364  dihjatb  42441  dihjatc  42442  dihjatcclem1  42443  dihjatcclem2  42444  dihjatcclem4  42446  dihjat  42448  dihjat3  42457  dihjat5N  42462  dvh4dimat  42463