Theorem atbase 40549

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 32979 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 2768	. . . 4 ⊢ (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
4	1, 3	sylnib 331	. . 3 ⊢ (𝑃 ∈ 𝐴 → ¬ (Atoms‘𝐾) = ∅)
5		fvprc 6903	. . 3 ⊢ (¬ 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
6	4, 5	nsyl2 142	. 2 ⊢ (𝑃 ∈ 𝐴 → 𝐾 ∈ V)
7		atombase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2763	. . . 4 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		eqid 2763	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	isat 40546	. . 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 2147  Vcvv 3454  ∅c0 4281   class class class wbr 5106  ‘cfv 6561  Basecbs 17419  0.cp0 18627   ⋖ ccvr 40522  Atomscatm 40523

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pr 5396

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-iota 6515  df-fun 6563  df-fv 6569  df-ats 40527

This theorem is used by:  atssbase  40550  0ltat  40551  leatb  40552  meetat  40556  atnle0  40569  atlen0  40570  atcmp  40571  atcvreq0  40574  atncvrN  40575  atnle  40577  atnem0  40578  atlatmstc  40579  atlatle  40580  cvlexch2  40589  cvlexchb1  40590  cvlexchb2  40591  cvlatexchb1  40594  cvlatexchb2  40595  cvlatexch1  40596  cvlatexch2  40597  cvlatexch3  40598  cvlcvr1  40599  cvlcvrp  40600  cvlatcvr1  40601  cvlatcvr2  40602  cvlsupr2  40603  cvlsupr7  40608  cvlsupr8  40609  hlatjcl  40627  hlatjcom  40628  hlatjidm  40629  hlatjass  40630  hlatj32  40632  hlatj4  40634  hlatlej1  40635  atnlej1  40639  atnlej2  40640  hlrelat5N  40661  hlrelat  40662  hlrelat2  40663  exatleN  40664  cvr2N  40671  hlrelat3  40672  cvrval3  40673  cvrval5  40675  cvrexchlem  40679  cvratlem  40681  cvrat  40682  atcvr0eq  40686  lnnat  40687  cvrat2  40689  atcvrneN  40690  atcvrj1  40691  atcvrj2b  40692  atltcvr  40695  atle  40696  atlelt  40698  2atlt  40699  atexchcvrN  40700  cvrat3  40702  cvrat4  40703  cvrat42  40704  2atjm  40705  atbtwn  40706  3noncolr2  40709  4noncolr3  40713  athgt  40716  3dim0  40717  3dimlem3a  40720  3dimlem3OLDN  40722  3dimlem4a  40723  3dimlem4OLDN  40725  3dim3  40729  2dim  40730  1cvratex  40733  1cvrjat  40735  1cvrat  40736  ps-1  40737  ps-2  40738  hlatexch3N  40740  hlatexch4  40741  ps-2b  40742  3atlem1  40743  3atlem2  40744  3atlem4  40746  3atlem5  40747  3atlem6  40748  3at  40750  islln3  40770  llnnleat  40773  llnn0  40776  llnle  40778  llnexatN  40781  llncmp  40782  2llnmat  40784  2at0mat0  40785  2atm  40787  ps-2c  40788  lplni2  40797  lplnle  40800  lplnnle2at  40801  lplnn0N  40807  islpln2a  40808  2atmat  40821  lplnexllnN  40824  2llnjaN  40826  2llnm4  40830  2llnmeqat  40831  lvoli3  40837  islvol5  40839  lvoli2  40841  lvolnle3at  40842  3atnelvolN  40846  lvoln0N  40851  islvol2aN  40852  4atlem3  40856  4atlem3a  40857  4atlem3b  40858  4atlem4a  40859  4atlem4b  40860  4atlem4c  40861  4atlem4d  40862  4atlem9  40863  4atlem10a  40864  4atlem10  40866  4atlem11a  40867  4atlem11b  40868  4atlem11  40869  4atlem12a  40870  4atlem12b  40871  4atlem12  40872  4at2  40874  lplncvrlvol2  40875  2lplnja  40879  dalempeb  40899  dalemqeb  40900  dalemreb  40901  dalemseb  40902  dalemteb  40903  dalemueb  40904  dalem3  40924  dalem16  40939  dalemcceb  40949  dalem21  40954  dalem25  40958  dalem38  40970  dalem39  40971  dalem43  40975  dalem44  40976  dalem45  40977  dalem53  40985  dalem54  40986  dalem55  40987  dalem57  40989  dalem60  40992  snatpsubN  41010  linepsubN  41012  pmaple  41021  pmapat  41023  pmap1N  41027  pmapsub  41028  pmapglbx  41029  isline2  41034  linepmap  41035  isline3  41036  isline4N  41037  lneq2at  41038  lncvrelatN  41041  lncmp  41043  2lnat  41044  2atm2atN  41045  2llnma1b  41046  2llnma1  41047  2llnma3r  41048  cdlema1N  41051  cdlemblem  41053  cdlemb  41054  elpaddn0  41060  paddcom  41073  paddasslem2  41081  paddasslem5  41084  paddasslem12  41091  paddasslem13  41092  pmapjoin  41112  pmapjat1  41113  pmapjat2  41114  pmapjlln1  41115  atmod1i1  41117  atmod1i2  41119  llnmod1i2  41120  atmod2i1  41121  atmod2i2  41122  atmod3i1  41124  atmod3i2  41125  atmod4i1  41126  atmod4i2  41127  llnexchb2lem  41128  llnexchb2  41129  dalawlem2  41132  dalawlem3  41133  dalawlem5  41135  dalawlem6  41136  dalawlem7  41137  dalawlem8  41138  dalawlem11  41141  dalawlem12  41142  polval2N  41166  pol1N  41170  polatN  41191  2polatN  41192  paddatclN  41209  linepsubclN  41211  lhp2lt  41261  lhp0lt  41263  lhpexle2lem  41269  lhpexle3lem  41271  lhpjat2  41281  lhpj1  41282  lhpmcvr3  41285  lhpmcvr4N  41286  lhpmcvr5N  41287  lhpmcvr6N  41288  lhpmatb  41291  lhp2at0  41292  lhp2atnle  41293  lhp2at0nle  41295  lhprelat3N  41300  lhple  41302  lhpat4N  41304  lhpat3  41306  4atexlemtlw  41327  4atexlemc  41329  4atexlemnclw  41330  4atexlemcnd  41332  4atex2-0aOLDN  41338  lauteq  41355  ltrnid  41395  ltrnel  41399  ltrnat  41400  ltrncnvat  41401  ltrncnvel  41402  ltrncoval  41405  ltrncnv  41406  ltrn11at  41407  ltrneq2  41408  ltrneq  41409  idltrn  41410  trlval2  41423  trlcnv  41425  trljat1  41426  trljat2  41427  ltrnideq  41435  arglem1N  41450  cdlemc1  41451  cdlemc2  41452  cdlemc4  41454  cdlemc5  41455  cdlemc6  41456  cdlemd1  41458  cdlemd2  41459  cdlemd3  41460  cdlemd4  41461  cdlemd7  41464  cdleme0aa  41470  cdleme0b  41472  cdleme0c  41473  cdleme0cp  41474  cdleme0cq  41475  cdleme0e  41477  cdleme0fN  41478  cdleme1b  41486  cdleme1  41487  cdleme2  41488  cdleme3b  41489  cdleme3c  41490  cdleme3e  41492  cdleme3g  41494  cdleme3h  41495  cdleme3  41497  cdleme5  41500  cdleme7d  41506  cdleme7e  41507  cdleme7ga  41508  cdleme7  41509  cdleme8  41510  cdleme9  41513  cdleme10  41514  cdleme11c  41521  cdleme11e  41523  cdleme11fN  41524  cdleme11g  41525  cdleme11k  41528  cdleme11  41530  cdleme15b  41535  cdleme15  41538  cdleme16b  41539  cdleme17b  41547  cdleme17c  41548  cdlemednpq  41559  cdleme20zN  41561  cdleme19a  41563  cdleme20bN  41570  cdleme20d  41572  cdleme20j  41578  cdleme21c  41587  cdleme22aa  41599  cdleme22b  41601  cdleme22cN  41602  cdleme22d  41603  cdleme22e  41604  cdleme22eALTN  41605  cdleme23b  41610  cdleme23c  41611  cdleme27N  41629  cdleme28a  41630  cdleme30a  41638  cdlemefrs29pre00  41655  cdlemefrs29bpre0  41656  cdlemefrs29cpre1  41658  cdlemefrs32fva  41660  cdlemefrs32fva1  41661  cdlemefr32snb  41665  cdlemefs32snb  41675  cdleme32snb  41696  cdleme32fva  41697  cdleme32fva1  41698  cdleme32fvaw  41699  cdleme35a  41708  cdleme35fnpq  41709  cdleme35b  41710  cdleme35c  41711  cdleme35f  41714  cdleme42c  41732  cdleme42e  41739  cdleme42h  41742  cdleme42i  41743  cdleme42ke  41745  cdleme42keg  41746  cdleme42mgN  41748  cdleme17d4  41757  cdleme48fvg  41760  cdleme48bw  41762  cdlemeg46req  41789  cdleme50trn3  41813  cdlemf1  41821  cdlemf2  41822  trlord  41829  ltrniotacnvval  41842  cdlemg2fv2  41860  cdlemg2l  41863  cdlemg7fvbwN  41867  cdlemg4c  41872  cdlemg4  41877  cdlemg6c  41880  cdlemg8b  41888  cdlemg11b  41902  cdlemg13a  41911  cdlemg17a  41921  cdlemg17h  41928  cdlemg17  41937  cdlemg18b  41939  cdlemg19a  41943  cdlemg27a  41952  cdlemg27b  41956  cdlemg31a  41957  cdlemg31b  41958  cdlemg31d  41960  cdlemg33b0  41961  cdlemg33a  41966  cdlemg35  41973  trlcolem  41986  cdlemg42  41989  cdlemg44a  41991  cdlemg46  41995  cdlemh1  42075  cdlemh2  42076  cdlemh  42077  cdlemi1  42078  cdlemi  42080  cdlemk3  42093  cdlemk4  42094  cdlemkvcl  42102  cdlemk7  42108  cdlemk11  42109  cdlemk15  42115  cdlemk1u  42119  cdlemk7u  42130  cdlemk11u  42131  cdlemk37  42174  cdlemk39  42176  cdlemkid1  42182  cdlemkid2  42184  cdlemk48  42210  cdlemk50  42212  cdlemk51  42213  cdlemk52  42214  dia2dimlem1  42324  dia2dimlem2  42325  dia2dimlem3  42326  dia2dimlem5  42328  dia2dimlem7  42330  dia2dimlem9  42332  dia2dimlem10  42333  dia2dimlem12  42335  dia2dimlem13  42336  cdlemm10N  42378  cdlemn2  42455  cdlemn3  42457  cdlemn9  42465  cdlemn10  42466  dihjustlem  42476  dihord1  42478  dihord2pre2  42486  dihvalcqat  42499  dib2dim  42503  dih2dimb  42504  dih2dimbALTN  42505  dihord5apre  42522  dihglbcpreN  42560  dihmeetlem3N  42565  dihmeetlem6  42569  dihjatc1  42571  dihjatc2N  42572  dihjatc3  42573  dihmeetlem9N  42575  dihmeetlem10N  42576  dihmeetlem11N  42577  dihmeetlem13N  42579  dihmeetlem15N  42581  dihmeetlem16N  42582  dihmeetlem17N  42583  dihatexv2  42599  dihjatb  42676  dihjatc  42677  dihjatcclem1  42678  dihjatcclem2  42679  dihjatcclem4  42681  dihjat  42683  dihjat3  42692  dihjat5N  42697  dvh4dimat  42698