Theorem atbase 40170

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 32833 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 4289	. . . 4 ⊢ (𝑃 ∈ 𝐴 → ¬ 𝐴 = ∅)
2		atombase.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
3	2	eqeq1i 2767	. . . 4 ⊢ (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
4	1, 3	sylnib 331	. . 3 ⊢ (𝑃 ∈ 𝐴 → ¬ (Atoms‘𝐾) = ∅)
5		fvprc 6874	. . 3 ⊢ (¬ 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
6	4, 5	nsyl2 142	. 2 ⊢ (𝑃 ∈ 𝐴 → 𝐾 ∈ V)
7		atombase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2762	. . . 4 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		eqid 2762	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	isat 40167	. . 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 3453  ∅c0 4282   class class class wbr 5107  ‘cfv 6537  Basecbs 17307  0.cp0 18515   ⋖ ccvr 40143  Atomscatm 40144

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6493  df-fun 6539  df-fv 6545  df-ats 40148

This theorem is used by:  atssbase  40171  0ltat  40172  leatb  40173  meetat  40177  atnle0  40190  atlen0  40191  atcmp  40192  atcvreq0  40195  atncvrN  40196  atnle  40198  atnem0  40199  atlatmstc  40200  atlatle  40201  cvlexch2  40210  cvlexchb1  40211  cvlexchb2  40212  cvlatexchb1  40215  cvlatexchb2  40216  cvlatexch1  40217  cvlatexch2  40218  cvlatexch3  40219  cvlcvr1  40220  cvlcvrp  40221  cvlatcvr1  40222  cvlatcvr2  40223  cvlsupr2  40224  cvlsupr7  40229  cvlsupr8  40230  hlatjcl  40248  hlatjcom  40249  hlatjidm  40250  hlatjass  40251  hlatj32  40253  hlatj4  40255  hlatlej1  40256  atnlej1  40260  atnlej2  40261  hlrelat5N  40282  hlrelat  40283  hlrelat2  40284  exatleN  40285  cvr2N  40292  hlrelat3  40293  cvrval3  40294  cvrval5  40296  cvrexchlem  40300  cvratlem  40302  cvrat  40303  atcvr0eq  40307  lnnat  40308  cvrat2  40310  atcvrneN  40311  atcvrj1  40312  atcvrj2b  40313  atltcvr  40316  atle  40317  atlelt  40319  2atlt  40320  atexchcvrN  40321  cvrat3  40323  cvrat4  40324  cvrat42  40325  2atjm  40326  atbtwn  40327  3noncolr2  40330  4noncolr3  40334  athgt  40337  3dim0  40338  3dimlem3a  40341  3dimlem3OLDN  40343  3dimlem4a  40344  3dimlem4OLDN  40346  3dim3  40350  2dim  40351  1cvratex  40354  1cvrjat  40356  1cvrat  40357  ps-1  40358  ps-2  40359  hlatexch3N  40361  hlatexch4  40362  ps-2b  40363  3atlem1  40364  3atlem2  40365  3atlem4  40367  3atlem5  40368  3atlem6  40369  3at  40371  islln3  40391  llnnleat  40394  llnn0  40397  llnle  40399  llnexatN  40402  llncmp  40403  2llnmat  40405  2at0mat0  40406  2atm  40408  ps-2c  40409  lplni2  40418  lplnle  40421  lplnnle2at  40422  lplnn0N  40428  islpln2a  40429  2atmat  40442  lplnexllnN  40445  2llnjaN  40447  2llnm4  40451  2llnmeqat  40452  lvoli3  40458  islvol5  40460  lvoli2  40462  lvolnle3at  40463  3atnelvolN  40467  lvoln0N  40472  islvol2aN  40473  4atlem3  40477  4atlem3a  40478  4atlem3b  40479  4atlem4a  40480  4atlem4b  40481  4atlem4c  40482  4atlem4d  40483  4atlem9  40484  4atlem10a  40485  4atlem10  40487  4atlem11a  40488  4atlem11b  40489  4atlem11  40490  4atlem12a  40491  4atlem12b  40492  4atlem12  40493  4at2  40495  lplncvrlvol2  40496  2lplnja  40500  dalempeb  40520  dalemqeb  40521  dalemreb  40522  dalemseb  40523  dalemteb  40524  dalemueb  40525  dalem3  40545  dalem16  40560  dalemcceb  40570  dalem21  40575  dalem25  40579  dalem38  40591  dalem39  40592  dalem43  40596  dalem44  40597  dalem45  40598  dalem53  40606  dalem54  40607  dalem55  40608  dalem57  40610  dalem60  40613  snatpsubN  40631  linepsubN  40633  pmaple  40642  pmapat  40644  pmap1N  40648  pmapsub  40649  pmapglbx  40650  isline2  40655  linepmap  40656  isline3  40657  isline4N  40658  lneq2at  40659  lncvrelatN  40662  lncmp  40664  2lnat  40665  2atm2atN  40666  2llnma1b  40667  2llnma1  40668  2llnma3r  40669  cdlema1N  40672  cdlemblem  40674  cdlemb  40675  elpaddn0  40681  paddcom  40694  paddasslem2  40702  paddasslem5  40705  paddasslem12  40712  paddasslem13  40713  pmapjoin  40733  pmapjat1  40734  pmapjat2  40735  pmapjlln1  40736  atmod1i1  40738  atmod1i2  40740  llnmod1i2  40741  atmod2i1  40742  atmod2i2  40743  atmod3i1  40745  atmod3i2  40746  atmod4i1  40747  atmod4i2  40748  llnexchb2lem  40749  llnexchb2  40750  dalawlem2  40753  dalawlem3  40754  dalawlem5  40756  dalawlem6  40757  dalawlem7  40758  dalawlem8  40759  dalawlem11  40762  dalawlem12  40763  polval2N  40787  pol1N  40791  polatN  40812  2polatN  40813  paddatclN  40830  linepsubclN  40832  lhp2lt  40882  lhp0lt  40884  lhpexle2lem  40890  lhpexle3lem  40892  lhpjat2  40902  lhpj1  40903  lhpmcvr3  40906  lhpmcvr4N  40907  lhpmcvr5N  40908  lhpmcvr6N  40909  lhpmatb  40912  lhp2at0  40913  lhp2atnle  40914  lhp2at0nle  40916  lhprelat3N  40921  lhple  40923  lhpat4N  40925  lhpat3  40927  4atexlemtlw  40948  4atexlemc  40950  4atexlemnclw  40951  4atexlemcnd  40953  4atex2-0aOLDN  40959  lauteq  40976  ltrnid  41016  ltrnel  41020  ltrnat  41021  ltrncnvat  41022  ltrncnvel  41023  ltrncoval  41026  ltrncnv  41027  ltrn11at  41028  ltrneq2  41029  ltrneq  41030  idltrn  41031  trlval2  41044  trlcnv  41046  trljat1  41047  trljat2  41048  ltrnideq  41056  arglem1N  41071  cdlemc1  41072  cdlemc2  41073  cdlemc4  41075  cdlemc5  41076  cdlemc6  41077  cdlemd1  41079  cdlemd2  41080  cdlemd3  41081  cdlemd4  41082  cdlemd7  41085  cdleme0aa  41091  cdleme0b  41093  cdleme0c  41094  cdleme0cp  41095  cdleme0cq  41096  cdleme0e  41098  cdleme0fN  41099  cdleme1b  41107  cdleme1  41108  cdleme2  41109  cdleme3b  41110  cdleme3c  41111  cdleme3e  41113  cdleme3g  41115  cdleme3h  41116  cdleme3  41118  cdleme5  41121  cdleme7d  41127  cdleme7e  41128  cdleme7ga  41129  cdleme7  41130  cdleme8  41131  cdleme9  41134  cdleme10  41135  cdleme11c  41142  cdleme11e  41144  cdleme11fN  41145  cdleme11g  41146  cdleme11k  41149  cdleme11  41151  cdleme15b  41156  cdleme15  41159  cdleme16b  41160  cdleme17b  41168  cdleme17c  41169  cdlemednpq  41180  cdleme20zN  41182  cdleme19a  41184  cdleme20bN  41191  cdleme20d  41193  cdleme20j  41199  cdleme21c  41208  cdleme22aa  41220  cdleme22b  41222  cdleme22cN  41223  cdleme22d  41224  cdleme22e  41225  cdleme22eALTN  41226  cdleme23b  41231  cdleme23c  41232  cdleme27N  41250  cdleme28a  41251  cdleme30a  41259  cdlemefrs29pre00  41276  cdlemefrs29bpre0  41277  cdlemefrs29cpre1  41279  cdlemefrs32fva  41281  cdlemefrs32fva1  41282  cdlemefr32snb  41286  cdlemefs32snb  41296  cdleme32snb  41317  cdleme32fva  41318  cdleme32fva1  41319  cdleme32fvaw  41320  cdleme35a  41329  cdleme35fnpq  41330  cdleme35b  41331  cdleme35c  41332  cdleme35f  41335  cdleme42c  41353  cdleme42e  41360  cdleme42h  41363  cdleme42i  41364  cdleme42ke  41366  cdleme42keg  41367  cdleme42mgN  41369  cdleme17d4  41378  cdleme48fvg  41381  cdleme48bw  41383  cdlemeg46req  41410  cdleme50trn3  41434  cdlemf1  41442  cdlemf2  41443  trlord  41450  ltrniotacnvval  41463  cdlemg2fv2  41481  cdlemg2l  41484  cdlemg7fvbwN  41488  cdlemg4c  41493  cdlemg4  41498  cdlemg6c  41501  cdlemg8b  41509  cdlemg11b  41523  cdlemg13a  41532  cdlemg17a  41542  cdlemg17h  41549  cdlemg17  41558  cdlemg18b  41560  cdlemg19a  41564  cdlemg27a  41573  cdlemg27b  41577  cdlemg31a  41578  cdlemg31b  41579  cdlemg31d  41581  cdlemg33b0  41582  cdlemg33a  41587  cdlemg35  41594  trlcolem  41607  cdlemg42  41610  cdlemg44a  41612  cdlemg46  41616  cdlemh1  41696  cdlemh2  41697  cdlemh  41698  cdlemi1  41699  cdlemi  41701  cdlemk3  41714  cdlemk4  41715  cdlemkvcl  41723  cdlemk7  41729  cdlemk11  41730  cdlemk15  41736  cdlemk1u  41740  cdlemk7u  41751  cdlemk11u  41752  cdlemk37  41795  cdlemk39  41797  cdlemkid1  41803  cdlemkid2  41805  cdlemk48  41831  cdlemk50  41833  cdlemk51  41834  cdlemk52  41835  dia2dimlem1  41945  dia2dimlem2  41946  dia2dimlem3  41947  dia2dimlem5  41949  dia2dimlem7  41951  dia2dimlem9  41953  dia2dimlem10  41954  dia2dimlem12  41956  dia2dimlem13  41957  cdlemm10N  41999  cdlemn2  42076  cdlemn3  42078  cdlemn9  42086  cdlemn10  42087  dihjustlem  42097  dihord1  42099  dihord2pre2  42107  dihvalcqat  42120  dib2dim  42124  dih2dimb  42125  dih2dimbALTN  42126  dihord5apre  42143  dihglbcpreN  42181  dihmeetlem3N  42186  dihmeetlem6  42190  dihjatc1  42192  dihjatc2N  42193  dihjatc3  42194  dihmeetlem9N  42196  dihmeetlem10N  42197  dihmeetlem11N  42198  dihmeetlem13N  42200  dihmeetlem15N  42202  dihmeetlem16N  42203  dihmeetlem17N  42204  dihatexv2  42220  dihjatb  42297  dihjatc  42298  dihjatcclem1  42299  dihjatcclem2  42300  dihjatcclem4  42302  dihjat  42304  dihjat3  42313  dihjat5N  42318  dvh4dimat  42319