Theorem atbase 35445

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 29775 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 4148	. . . 4 ⊢ (𝑃 ∈ 𝐴 → ¬ 𝐴 = ∅)
2		atombase.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
3	2	eqeq1i 2783	. . . 4 ⊢ (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
4	1, 3	sylnib 320	. . 3 ⊢ (𝑃 ∈ 𝐴 → ¬ (Atoms‘𝐾) = ∅)
5		fvprc 6439	. . 3 ⊢ (¬ 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
6	4, 5	nsyl2 145	. 2 ⊢ (𝑃 ∈ 𝐴 → 𝐾 ∈ V)
7		atombase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2778	. . . 4 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		eqid 2778	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	isat 35442	. . 3 ⊢ (𝐾 ∈ V → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
11	10	simprbda 494	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐵)
12	6, 11	mpancom 678	1 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1601   ∈ wcel 2107  Vcvv 3398  ∅c0 4141   class class class wbr 4886  ‘cfv 6135  Basecbs 16255  0.cp0 17423   ⋖ ccvr 35418  Atomscatm 35419

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-iota 6099  df-fun 6137  df-fv 6143  df-ats 35423

This theorem is referenced by:  atssbase  35446  0ltat  35447  leatb  35448  meetat  35452  atnle0  35465  atlen0  35466  atcmp  35467  atcvreq0  35470  atncvrN  35471  atnle  35473  atnem0  35474  atlatmstc  35475  atlatle  35476  cvlexch2  35485  cvlexchb1  35486  cvlexchb2  35487  cvlatexchb1  35490  cvlatexchb2  35491  cvlatexch1  35492  cvlatexch2  35493  cvlatexch3  35494  cvlcvr1  35495  cvlcvrp  35496  cvlatcvr1  35497  cvlatcvr2  35498  cvlsupr2  35499  cvlsupr7  35504  cvlsupr8  35505  hlatjcl  35523  hlatjcom  35524  hlatjidm  35525  hlatjass  35526  hlatj32  35528  hlatj4  35530  hlatlej1  35531  atnlej1  35535  atnlej2  35536  hlrelat5N  35557  hlrelat  35558  hlrelat2  35559  exatleN  35560  cvr2N  35567  hlrelat3  35568  cvrval3  35569  cvrval5  35571  cvrexchlem  35575  cvratlem  35577  cvrat  35578  atcvr0eq  35582  lnnat  35583  cvrat2  35585  atcvrneN  35586  atcvrj1  35587  atcvrj2b  35588  atltcvr  35591  atle  35592  atlelt  35594  2atlt  35595  atexchcvrN  35596  cvrat3  35598  cvrat4  35599  cvrat42  35600  2atjm  35601  atbtwn  35602  3noncolr2  35605  4noncolr3  35609  athgt  35612  3dim0  35613  3dimlem3a  35616  3dimlem3OLDN  35618  3dimlem4a  35619  3dimlem4OLDN  35621  3dim3  35625  2dim  35626  1cvratex  35629  1cvrjat  35631  1cvrat  35632  ps-1  35633  ps-2  35634  hlatexch3N  35636  hlatexch4  35637  ps-2b  35638  3atlem1  35639  3atlem2  35640  3atlem4  35642  3atlem5  35643  3atlem6  35644  3at  35646  islln3  35666  llnnleat  35669  llnn0  35672  llnle  35674  llnexatN  35677  llncmp  35678  2llnmat  35680  2at0mat0  35681  2atm  35683  ps-2c  35684  lplni2  35693  lplnle  35696  lplnnle2at  35697  lplnn0N  35703  islpln2a  35704  2atmat  35717  lplnexllnN  35720  2llnjaN  35722  2llnm4  35726  2llnmeqat  35727  lvoli3  35733  islvol5  35735  lvoli2  35737  lvolnle3at  35738  3atnelvolN  35742  lvoln0N  35747  islvol2aN  35748  4atlem3  35752  4atlem3a  35753  4atlem3b  35754  4atlem4a  35755  4atlem4b  35756  4atlem4c  35757  4atlem4d  35758  4atlem9  35759  4atlem10a  35760  4atlem10  35762  4atlem11a  35763  4atlem11b  35764  4atlem11  35765  4atlem12a  35766  4atlem12b  35767  4atlem12  35768  4at2  35770  lplncvrlvol2  35771  2lplnja  35775  dalempeb  35795  dalemqeb  35796  dalemreb  35797  dalemseb  35798  dalemteb  35799  dalemueb  35800  dalem3  35820  dalem16  35835  dalemcceb  35845  dalem21  35850  dalem25  35854  dalem38  35866  dalem39  35867  dalem43  35871  dalem44  35872  dalem45  35873  dalem53  35881  dalem54  35882  dalem55  35883  dalem57  35885  dalem60  35888  snatpsubN  35906  linepsubN  35908  pmaple  35917  pmapat  35919  pmap1N  35923  pmapsub  35924  pmapglbx  35925  isline2  35930  linepmap  35931  isline3  35932  isline4N  35933  lneq2at  35934  lncvrelatN  35937  lncmp  35939  2lnat  35940  2atm2atN  35941  2llnma1b  35942  2llnma1  35943  2llnma3r  35944  cdlema1N  35947  cdlemblem  35949  cdlemb  35950  elpaddn0  35956  paddcom  35969  paddasslem2  35977  paddasslem5  35980  paddasslem12  35987  paddasslem13  35988  pmapjoin  36008  pmapjat1  36009  pmapjat2  36010  pmapjlln1  36011  atmod1i1  36013  atmod1i2  36015  llnmod1i2  36016  atmod2i1  36017  atmod2i2  36018  atmod3i1  36020  atmod3i2  36021  atmod4i1  36022  atmod4i2  36023  llnexchb2lem  36024  llnexchb2  36025  dalawlem2  36028  dalawlem3  36029  dalawlem5  36031  dalawlem6  36032  dalawlem7  36033  dalawlem8  36034  dalawlem11  36037  dalawlem12  36038  polval2N  36062  pol1N  36066  polatN  36087  2polatN  36088  paddatclN  36105  linepsubclN  36107  lhp2lt  36157  lhp0lt  36159  lhpexle2lem  36165  lhpexle3lem  36167  lhpjat2  36177  lhpj1  36178  lhpmcvr3  36181  lhpmcvr4N  36182  lhpmcvr5N  36183  lhpmcvr6N  36184  lhpmatb  36187  lhp2at0  36188  lhp2atnle  36189  lhp2at0nle  36191  lhprelat3N  36196  lhple  36198  lhpat4N  36200  lhpat3  36202  4atexlemtlw  36223  4atexlemc  36225  4atexlemnclw  36226  4atexlemcnd  36228  4atex2-0aOLDN  36234  lauteq  36251  ltrnid  36291  ltrnel  36295  ltrnat  36296  ltrncnvat  36297  ltrncnvel  36298  ltrncoval  36301  ltrncnv  36302  ltrn11at  36303  ltrneq2  36304  ltrneq  36305  idltrn  36306  trlval2  36319  trlcnv  36321  trljat1  36322  trljat2  36323  ltrnideq  36331  arglem1N  36346  cdlemc1  36347  cdlemc2  36348  cdlemc4  36350  cdlemc5  36351  cdlemc6  36352  cdlemd1  36354  cdlemd2  36355  cdlemd3  36356  cdlemd4  36357  cdlemd7  36360  cdleme0aa  36366  cdleme0b  36368  cdleme0c  36369  cdleme0cp  36370  cdleme0cq  36371  cdleme0e  36373  cdleme0fN  36374  cdleme1b  36382  cdleme1  36383  cdleme2  36384  cdleme3b  36385  cdleme3c  36386  cdleme3e  36388  cdleme3g  36390  cdleme3h  36391  cdleme3  36393  cdleme5  36396  cdleme7d  36402  cdleme7e  36403  cdleme7ga  36404  cdleme7  36405  cdleme8  36406  cdleme9  36409  cdleme10  36410  cdleme11c  36417  cdleme11e  36419  cdleme11fN  36420  cdleme11g  36421  cdleme11k  36424  cdleme11  36426  cdleme15b  36431  cdleme15  36434  cdleme16b  36435  cdleme17b  36443  cdleme17c  36444  cdlemednpq  36455  cdleme20zN  36457  cdleme19a  36459  cdleme20bN  36466  cdleme20d  36468  cdleme20j  36474  cdleme21c  36483  cdleme22aa  36495  cdleme22b  36497  cdleme22cN  36498  cdleme22d  36499  cdleme22e  36500  cdleme22eALTN  36501  cdleme23b  36506  cdleme23c  36507  cdleme27N  36525  cdleme28a  36526  cdleme30a  36534  cdlemefrs29pre00  36551  cdlemefrs29bpre0  36552  cdlemefrs29cpre1  36554  cdlemefrs32fva  36556  cdlemefrs32fva1  36557  cdlemefr32snb  36561  cdlemefs32snb  36571  cdleme32snb  36592  cdleme32fva  36593  cdleme32fva1  36594  cdleme32fvaw  36595  cdleme35a  36604  cdleme35fnpq  36605  cdleme35b  36606  cdleme35c  36607  cdleme35f  36610  cdleme42c  36628  cdleme42e  36635  cdleme42h  36638  cdleme42i  36639  cdleme42ke  36641  cdleme42keg  36642  cdleme42mgN  36644  cdleme17d4  36653  cdleme48fvg  36656  cdleme48bw  36658  cdlemeg46req  36685  cdleme50trn3  36709  cdlemf1  36717  cdlemf2  36718  trlord  36725  ltrniotacnvval  36738  cdlemg2fv2  36756  cdlemg2l  36759  cdlemg7fvbwN  36763  cdlemg4c  36768  cdlemg4  36773  cdlemg6c  36776  cdlemg8b  36784  cdlemg11b  36798  cdlemg13a  36807  cdlemg17a  36817  cdlemg17h  36824  cdlemg17  36833  cdlemg18b  36835  cdlemg19a  36839  cdlemg27a  36848  cdlemg27b  36852  cdlemg31a  36853  cdlemg31b  36854  cdlemg31d  36856  cdlemg33b0  36857  cdlemg33a  36862  cdlemg35  36869  trlcolem  36882  cdlemg42  36885  cdlemg44a  36887  cdlemg46  36891  cdlemh1  36971  cdlemh2  36972  cdlemh  36973  cdlemi1  36974  cdlemi  36976  cdlemk3  36989  cdlemk4  36990  cdlemkvcl  36998  cdlemk7  37004  cdlemk11  37005  cdlemk15  37011  cdlemk1u  37015  cdlemk7u  37026  cdlemk11u  37027  cdlemk37  37070  cdlemk39  37072  cdlemkid1  37078  cdlemkid2  37080  cdlemk48  37106  cdlemk50  37108  cdlemk51  37109  cdlemk52  37110  dia2dimlem1  37220  dia2dimlem2  37221  dia2dimlem3  37222  dia2dimlem5  37224  dia2dimlem7  37226  dia2dimlem9  37228  dia2dimlem10  37229  dia2dimlem12  37231  dia2dimlem13  37232  cdlemm10N  37274  cdlemn2  37351  cdlemn3  37353  cdlemn9  37361  cdlemn10  37362  dihjustlem  37372  dihord1  37374  dihord2pre2  37382  dihvalcqat  37395  dib2dim  37399  dih2dimb  37400  dih2dimbALTN  37401  dihord5apre  37418  dihglbcpreN  37456  dihmeetlem3N  37461  dihmeetlem6  37465  dihjatc1  37467  dihjatc2N  37468  dihjatc3  37469  dihmeetlem9N  37471  dihmeetlem10N  37472  dihmeetlem11N  37473  dihmeetlem13N  37475  dihmeetlem15N  37477  dihmeetlem16N  37478  dihmeetlem17N  37479  dihatexv2  37495  dihjatb  37572  dihjatc  37573  dihjatcclem1  37574  dihjatcclem2  37575  dihjatcclem4  37577  dihjat  37579  dihjat3  37588  dihjat5N  37593  dvh4dimat  37594